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  4655  sucunielr  4657  ordsuc  4710  peano2b  4762  xpiindim  4917  fununfun  5424  fvelrnb  5750  fliftcnv  6001  riotaprop  6064  unielxp  6408  dmtpos  6527  tpossym  6547  ercnv  6828  cnvct  7097  php5dom  7164  3xpfi  7241  recrecnq  7762  1idpr  7960  eqlei2  8422  lem1  9180  eluzfz1  10446  fzpred  10488  uznfz  10521  fz0fzdiffz0  10548  fzctr  10551  flid  10733  flqeqceilz  10769  faclbnd3  11196  bcn1  11211  isfinite4im  11246  hashfac  11303  leabs  11855  gcd0id  12774  lcmgcdlem  12873  dvdsnprmd  12921  pcprod  13147  fldivp1  13149  intopsn  13738  mgm1  13741  sgrp1  13777  mnd1  13813  mnd1id  13814  grp1  13962  grp1inv  13963  eqger  14078  eqgid  14080  qusghm  14136  rngressid  14304  ring1  14415  ringressid  14419  subrgsubm  14593  resrhm2b  14608  lssex  14742  cncrng  14957  ressascl  15090  psrbagfsupp  15106  psrbaglesupp  15109  eltpsg  15193  tg1  15212  cldval  15252  cldss  15258  cldopn  15260  psmetdmdm  15477  dvef  15880  relogef  16018  zabsle1  16240  usgredg2vlem2  16586  wlkprop  16690  wlkvtxiedg  16708  eupthseg  16815  bj-nn0suc0  17098