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  3115  onsucelsucr  4601  sucunielr  4603  ordsuc  4656  peano2b  4708  xpiindim  4862  fununfun  5367  fvelrnb  5686  fliftcnv  5928  riotaprop  5989  unielxp  6329  dmtpos  6413  tpossym  6433  ercnv  6714  cnvct  6975  php5dom  7037  3xpfi  7111  recrecnq  7597  1idpr  7795  eqlei2  8257  lem1  9010  eluzfz1  10244  fzpred  10283  uznfz  10316  fz0fzdiffz0  10343  fzctr  10346  flid  10521  flqeqceilz  10557  faclbnd3  10982  bcn1  10997  isfinite4im  11031  leabs  11606  gcd0id  12521  lcmgcdlem  12620  dvdsnprmd  12668  pcprod  12890  fldivp1  12892  intopsn  13421  mgm1  13424  sgrp1  13465  mnd1  13509  mnd1id  13510  grp1  13660  grp1inv  13661  eqger  13782  eqgid  13784  qusghm  13840  rngressid  13938  ring1  14043  ringressid  14047  subrgsubm  14219  resrhm2b  14234  lssex  14339  cncrng  14554  eltpsg  14735  tg1  14754  cldval  14794  cldss  14800  cldopn  14802  psmetdmdm  15019  dvef  15422  relogef  15559  zabsle1  15699  usgredg2vlem2  16042  wlkprop  16099  wlkvtxiedg  16117  bj-nn0suc0  16422