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  3128  onsucelsucr  4629  sucunielr  4631  ordsuc  4684  peano2b  4736  xpiindim  4891  fununfun  5398  fvelrnb  5723  fliftcnv  5967  riotaprop  6028  unielxp  6367  dmtpos  6486  tpossym  6506  ercnv  6787  cnvct  7049  php5dom  7116  3xpfi  7193  recrecnq  7708  1idpr  7906  eqlei2  8367  lem1  9120  eluzfz1  10364  fzpred  10403  uznfz  10436  fz0fzdiffz0  10463  fzctr  10466  flid  10643  flqeqceilz  10679  faclbnd3  11104  bcn1  11119  isfinite4im  11153  leabs  11755  gcd0id  12671  lcmgcdlem  12770  dvdsnprmd  12818  pcprod  13040  fldivp1  13042  intopsn  13572  mgm1  13575  sgrp1  13616  mnd1  13660  mnd1id  13661  grp1  13811  grp1inv  13812  eqger  13933  eqgid  13935  qusghm  13991  rngressid  14090  ring1  14195  ringressid  14199  subrgsubm  14371  resrhm2b  14386  lssex  14494  cncrng  14709  psrbagfsupp  14811  psrbaglesupp  14814  eltpsg  14897  tg1  14916  cldval  14956  cldss  14962  cldopn  14964  psmetdmdm  15181  dvef  15584  relogef  15721  zabsle1  15864  usgredg2vlem2  16210  wlkprop  16314  wlkvtxiedg  16332  eupthseg  16439  bj-nn0suc0  16712