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  9141  eluzfz1  10388  fzpred  10429  uznfz  10462  fz0fzdiffz0  10489  fzctr  10492  flid  10671  flqeqceilz  10707  faclbnd3  11133  bcn1  11148  isfinite4im  11183  leabs  11788  gcd0id  12704  lcmgcdlem  12803  dvdsnprmd  12851  pcprod  13073  fldivp1  13075  intopsn  13634  mgm1  13637  sgrp1  13678  mnd1  13714  mnd1id  13715  grp1  13865  grp1inv  13866  eqger  13981  eqgid  13983  qusghm  14039  rngressid  14197  ring1  14306  ringressid  14310  subrgsubm  14484  resrhm2b  14499  lssex  14632  cncrng  14847  psrbagfsupp  14949  psrbaglesupp  14952  eltpsg  15035  tg1  15054  cldval  15094  cldss  15100  cldopn  15102  psmetdmdm  15319  dvef  15722  relogef  15859  zabsle1  16002  usgredg2vlem2  16348  wlkprop  16452  wlkvtxiedg  16470  eupthseg  16577  bj-nn0suc0  16860