Theorem mpancom 426

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpan  428  spesbc  3138  onsucelsucr  4655  sucunielr  4657  ordsuc  4710  peano2b  4762  xpiindim  4917  fununfun  5424  fvelrnb  5750  fliftcnv  6001  riotaprop  6064  unielxp  6408  dmtpos  6527  tpossym  6547  ercnv  6828  cnvct  7097  php5dom  7164  3xpfi  7241  recrecnq  7761  1idpr  7959  eqlei2  8420  lem1  9178  eluzfz1  10437  fzpred  10479  uznfz  10512  fz0fzdiffz0  10539  fzctr  10542  flid  10721  flqeqceilz  10757  faclbnd3  11183  bcn1  11198  isfinite4im  11233  hashfac  11290  leabs  11842  gcd0id  12758  lcmgcdlem  12857  dvdsnprmd  12905  pcprod  13127  fldivp1  13129  intopsn  13689  mgm1  13692  sgrp1  13728  mnd1  13764  mnd1id  13765  grp1  13913  grp1inv  13914  eqger  14029  eqgid  14031  qusghm  14087  rngressid  14255  ring1  14366  ringressid  14370  subrgsubm  14544  resrhm2b  14559  lssex  14693  cncrng  14908  ressascl  15041  psrbagfsupp  15057  psrbaglesupp  15060  eltpsg  15143  tg1  15162  cldval  15202  cldss  15208  cldopn  15210  psmetdmdm  15427  dvef  15830  relogef  15968  zabsle1  16130  usgredg2vlem2  16476  wlkprop  16580  wlkvtxiedg  16598  eupthseg  16705  bj-nn0suc0  16988