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  3118  onsucelsucr  4606  sucunielr  4608  ordsuc  4661  peano2b  4713  xpiindim  4867  fununfun  5373  fvelrnb  5693  fliftcnv  5936  riotaprop  5997  unielxp  6337  dmtpos  6422  tpossym  6442  ercnv  6723  cnvct  6984  php5dom  7049  3xpfi  7126  recrecnq  7614  1idpr  7812  eqlei2  8274  lem1  9027  eluzfz1  10266  fzpred  10305  uznfz  10338  fz0fzdiffz0  10365  fzctr  10368  flid  10545  flqeqceilz  10581  faclbnd3  11006  bcn1  11021  isfinite4im  11055  leabs  11639  gcd0id  12555  lcmgcdlem  12654  dvdsnprmd  12702  pcprod  12924  fldivp1  12926  intopsn  13455  mgm1  13458  sgrp1  13499  mnd1  13543  mnd1id  13544  grp1  13694  grp1inv  13695  eqger  13816  eqgid  13818  qusghm  13874  rngressid  13973  ring1  14078  ringressid  14082  subrgsubm  14254  resrhm2b  14269  lssex  14374  cncrng  14589  eltpsg  14770  tg1  14789  cldval  14829  cldss  14835  cldopn  14837  psmetdmdm  15054  dvef  15457  relogef  15594  zabsle1  15734  usgredg2vlem2  16080  wlkprop  16184  wlkvtxiedg  16202  eupthseg  16309  bj-nn0suc0  16571