Theorem mpancom 416

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 406	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpan  418  spesbc  2946  onsucelsucr  4362  sucunielr  4364  ordsuc  4416  peano2b  4466  xpiindim  4614  fvelrnb  5401  fliftcnv  5628  riotaprop  5685  unielxp  6002  dmtpos  6083  tpossym  6103  ercnv  6380  cnvct  6633  php5dom  6686  3xpfi  6748  recrecnq  7103  1idpr  7301  eqlei2  7729  lem1  8463  eluzfz1  9652  fzpred  9691  uznfz  9724  fz0fzdiffz0  9748  fzctr  9751  flid  9898  flqeqceilz  9932  faclbnd3  10330  bcn1  10345  isfinite4im  10380  leabs  10686  gcd0id  11462  lcmgcdlem  11551  dvdsnprmd  11599  eltpsg  11989  tg1  12010  cldval  12050  cldss  12056  cldopn  12058  psmetdmdm  12252  bj-nn0suc0  12733