Theorem mpancom 422

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mpan  424  spesbc  3132  onsucelsucr  4635  sucunielr  4637  ordsuc  4690  peano2b  4742  xpiindim  4897  fununfun  5404  fvelrnb  5729  fliftcnv  5974  riotaprop  6037  unielxp  6381  dmtpos  6500  tpossym  6520  ercnv  6801  cnvct  7063  php5dom  7130  3xpfi  7207  recrecnq  7725  1idpr  7923  eqlei2  8384  lem1  9138  eluzfz1  10385  fzpred  10426  uznfz  10459  fz0fzdiffz0  10486  fzctr  10489  flid  10668  flqeqceilz  10704  faclbnd3  11130  bcn1  11145  isfinite4im  11180  leabs  11784  gcd0id  12700  lcmgcdlem  12799  dvdsnprmd  12847  pcprod  13069  fldivp1  13071  intopsn  13664  mgm1  13667  sgrp1  13708  mnd1  13752  mnd1id  13753  grp1  13903  grp1inv  13904  eqger  14025  eqgid  14027  qusghm  14083  rngressid  14182  ring1  14287  ringressid  14291  subrgsubm  14465  resrhm2b  14480  lssex  14614  cncrng  14829  psrbagfsupp  14931  psrbaglesupp  14934  eltpsg  15017  tg1  15036  cldval  15076  cldss  15082  cldopn  15084  psmetdmdm  15301  dvef  15704  relogef  15841  zabsle1  15984  usgredg2vlem2  16330  wlkprop  16434  wlkvtxiedg  16452  eupthseg  16559  bj-nn0suc0  16832