Theorem mpancom 426

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpan  428  spesbc  3138  onsucelsucr  4657  sucunielr  4659  ordsuc  4712  peano2b  4764  xpiindim  4919  fununfun  5427  fvelrnb  5753  fliftcnv  6004  riotaprop  6067  unielxp  6412  dmtpos  6531  tpossym  6551  ercnv  6832  cnvct  7102  php5dom  7169  3xpfi  7246  recrecnq  7768  1idpr  7966  eqlei2  8428  lem1  9186  eluzfz1  10453  fzpred  10495  uznfz  10528  fz0fzdiffz0  10555  fzctr  10558  flid  10741  flqeqceilz  10777  faclbnd3  11204  bcn1  11219  isfinite4im  11254  hashfac  11311  leabs  11863  gcd0id  12782  lcmgcdlem  12881  dvdsnprmd  12929  pcprod  13155  fldivp1  13157  intopsn  13747  mgm1  13750  sgrp1  13786  mnd1  13822  mnd1id  13823  grp1  13971  grp1inv  13972  eqger  14087  eqgid  14089  qusghm  14145  cntzrcl  14160  rngressid  14361  ring1  14472  ringressid  14478  subrgsubm  14652  resrhm2b  14667  lssex  14801  cncrng  15016  ressascl  15149  psrbagfsupp  15167  psrbaglesupp  15173  eltpsg  15278  tg1  15297  cldval  15337  cldss  15343  cldopn  15345  psmetdmdm  15562  dvef  15965  relogef  16105  bposlem7  16329  zabsle1  16335  usgredg2vlem2  16681  wlkprop  16785  wlkvtxiedg  16803  eupthseg  16910  bj-nn0suc0  17193