Theorem mpancom 413

Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpancom.1	⊢ (𝜓 → 𝜑)
mpancom.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpancom	⊢ (𝜓 → 𝜒)

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 ⊢ (𝜓 → 𝜑)
2		id 19	. 2 ⊢ (𝜓 → 𝜓)
3		mpancom.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 403	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  mpan  414  spesbc  2899  onsucelsucr  4252  sucunielr  4254  ordsuc  4306  peano2b  4355  xpiindim  4491  fvelrnb  5242  fliftcnv  5455  riotaprop  5511  unielxp  5820  dmtpos  5894  tpossym  5914  ercnv  6150  php5dom  6349  recrecnq  6584  1idpr  6782  eqlei2  7205  lem1  7925  eluzfz1  9050  fzpred  9087  uznfz  9120  fz0fzdiffz0  9141  fzctr  9144  flid  9286  flqeqceilz  9320  faclbnd3  9670  bcn1  9685  leabs  9960  gcd0id  10370  lcmgcdlem  10459  dvdsnprmd  10507  bj-nn0suc0  10745