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

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  428  spesbc  3138  onsucelsucr  4653  sucunielr  4655  ordsuc  4708  peano2b  4760  xpiindim  4915  fununfun  5422  fvelrnb  5747  fliftcnv  5995  riotaprop  6058  unielxp  6402  dmtpos  6521  tpossym  6541  ercnv  6822  cnvct  7091  php5dom  7158  3xpfi  7235  recrecnq  7755  1idpr  7953  eqlei2  8414  lem1  9171  eluzfz1  10418  fzpred  10460  uznfz  10493  fz0fzdiffz0  10520  fzctr  10523  flid  10702  flqeqceilz  10738  faclbnd3  11164  bcn1  11179  isfinite4im  11214  hashfac  11271  leabs  11823  gcd0id  12739  lcmgcdlem  12838  dvdsnprmd  12886  pcprod  13108  fldivp1  13110  intopsn  13670  mgm1  13673  sgrp1  13709  mnd1  13745  mnd1id  13746  grp1  13894  grp1inv  13895  eqger  14010  eqgid  14012  qusghm  14068  rngressid  14236  ring1  14347  ringressid  14351  subrgsubm  14525  resrhm2b  14540  lssex  14674  cncrng  14889  ressascl  15022  psrbagfsupp  15038  psrbaglesupp  15041  eltpsg  15124  tg1  15143  cldval  15183  cldss  15189  cldopn  15191  psmetdmdm  15408  dvef  15811  relogef  15948  zabsle1  16101  usgredg2vlem2  16447  wlkprop  16551  wlkvtxiedg  16569  eupthseg  16676  bj-nn0suc0  16959