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  3116  onsucelsucr  4604  sucunielr  4606  ordsuc  4659  peano2b  4711  xpiindim  4865  fununfun  5370  fvelrnb  5689  fliftcnv  5931  riotaprop  5992  unielxp  6332  dmtpos  6417  tpossym  6437  ercnv  6718  cnvct  6979  php5dom  7044  3xpfi  7120  recrecnq  7607  1idpr  7805  eqlei2  8267  lem1  9020  eluzfz1  10259  fzpred  10298  uznfz  10331  fz0fzdiffz0  10358  fzctr  10361  flid  10537  flqeqceilz  10573  faclbnd3  10998  bcn1  11013  isfinite4im  11047  leabs  11628  gcd0id  12543  lcmgcdlem  12642  dvdsnprmd  12690  pcprod  12912  fldivp1  12914  intopsn  13443  mgm1  13446  sgrp1  13487  mnd1  13531  mnd1id  13532  grp1  13682  grp1inv  13683  eqger  13804  eqgid  13806  qusghm  13862  rngressid  13960  ring1  14065  ringressid  14069  subrgsubm  14241  resrhm2b  14256  lssex  14361  cncrng  14576  eltpsg  14757  tg1  14776  cldval  14816  cldss  14822  cldopn  14824  psmetdmdm  15041  dvef  15444  relogef  15581  zabsle1  15721  usgredg2vlem2  16067  wlkprop  16138  wlkvtxiedg  16156  eupthseg  16261  bj-nn0suc0  16495