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  4492  sucunielr  4494  ordsuc  4547  peano2b  4599  xpiindim  4748  fvelrnb  5544  fliftcnv  5774  riotaprop  5832  unielxp  6153  dmtpos  6235  tpossym  6255  ercnv  6534  cnvct  6787  php5dom  6841  3xpfi  6908  recrecnq  7356  1idpr  7554  eqlei2  8014  lem1  8763  eluzfz1  9987  fzpred  10026  uznfz  10059  fz0fzdiffz0  10086  fzctr  10089  flid  10240  flqeqceilz  10274  faclbnd3  10677  bcn1  10692  isfinite4im  10727  leabs  11038  gcd0id  11934  lcmgcdlem  12031  dvdsnprmd  12079  pcprod  12298  fldivp1  12300  intopsn  12621  mgm1  12624  sgrp1  12651  mnd1  12679  mnd1id  12680  eltpsg  12832  tg1  12853  cldval  12893  cldss  12899  cldopn  12901  psmetdmdm  13118  dvef  13482  relogef  13579  zabsle1  13694  bj-nn0suc0  13985