Theorem mpancom 420

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 409	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mpan  422  spesbc  3040  onsucelsucr  4490  sucunielr  4492  ordsuc  4545  peano2b  4597  xpiindim  4746  fvelrnb  5542  fliftcnv  5772  riotaprop  5830  unielxp  6151  dmtpos  6233  tpossym  6253  ercnv  6531  cnvct  6784  php5dom  6838  3xpfi  6905  recrecnq  7345  1idpr  7543  eqlei2  8003  lem1  8752  eluzfz1  9976  fzpred  10015  uznfz  10048  fz0fzdiffz0  10075  fzctr  10078  flid  10229  flqeqceilz  10263  faclbnd3  10666  bcn1  10681  isfinite4im  10716  leabs  11027  gcd0id  11923  lcmgcdlem  12020  dvdsnprmd  12068  pcprod  12287  fldivp1  12289  intopsn  12610  mgm1  12613  sgrp1  12640  mnd1  12668  mnd1id  12669  eltpsg  12793  tg1  12814  cldval  12854  cldss  12860  cldopn  12862  psmetdmdm  13079  dvef  13443  relogef  13540  zabsle1  13655  bj-nn0suc0  13947