Theorem mpancom 418

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpan  420  spesbc  2994  onsucelsucr  4424  sucunielr  4426  ordsuc  4478  peano2b  4528  xpiindim  4676  fvelrnb  5469  fliftcnv  5696  riotaprop  5753  unielxp  6072  dmtpos  6153  tpossym  6173  ercnv  6450  cnvct  6703  php5dom  6757  3xpfi  6819  recrecnq  7202  1idpr  7400  eqlei2  7858  lem1  8605  eluzfz1  9811  fzpred  9850  uznfz  9883  fz0fzdiffz0  9907  fzctr  9910  flid  10057  flqeqceilz  10091  faclbnd3  10489  bcn1  10504  isfinite4im  10539  leabs  10846  gcd0id  11667  lcmgcdlem  11758  dvdsnprmd  11806  eltpsg  12207  tg1  12228  cldval  12268  cldss  12274  cldopn  12276  psmetdmdm  12493  dvef  12856  bj-nn0suc0  13148