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  3048  onsucelsucr  4505  sucunielr  4507  ordsuc  4560  peano2b  4612  xpiindim  4761  fvelrnb  5560  fliftcnv  5791  riotaprop  5849  unielxp  6170  dmtpos  6252  tpossym  6272  ercnv  6551  cnvct  6804  php5dom  6858  3xpfi  6925  recrecnq  7388  1idpr  7586  eqlei2  8046  lem1  8798  eluzfz1  10024  fzpred  10063  uznfz  10096  fz0fzdiffz0  10123  fzctr  10126  flid  10277  flqeqceilz  10311  faclbnd3  10714  bcn1  10729  isfinite4im  10763  leabs  11074  gcd0id  11970  lcmgcdlem  12067  dvdsnprmd  12115  pcprod  12334  fldivp1  12336  intopsn  12716  mgm1  12719  sgrp1  12746  mnd1  12775  mnd1id  12776  grp1  12904  grp1inv  12905  ring1  13136  cncrng  13268  eltpsg  13320  tg1  13341  cldval  13381  cldss  13387  cldopn  13389  psmetdmdm  13606  dvef  13970  relogef  14067  zabsle1  14182  bj-nn0suc0  14473