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  3071  onsucelsucr  4540  sucunielr  4542  ordsuc  4595  peano2b  4647  xpiindim  4799  fvelrnb  5604  fliftcnv  5838  riotaprop  5897  unielxp  6227  dmtpos  6309  tpossym  6329  ercnv  6608  cnvct  6863  php5dom  6919  3xpfi  6987  recrecnq  7454  1idpr  7652  eqlei2  8114  lem1  8866  eluzfz1  10097  fzpred  10136  uznfz  10169  fz0fzdiffz0  10196  fzctr  10199  flid  10353  flqeqceilz  10389  faclbnd3  10814  bcn1  10829  isfinite4im  10863  leabs  11218  gcd0id  12116  lcmgcdlem  12215  dvdsnprmd  12263  pcprod  12484  fldivp1  12486  intopsn  12950  mgm1  12953  sgrp1  12994  mnd1  13027  mnd1id  13028  grp1  13178  grp1inv  13179  eqger  13294  eqgid  13296  qusghm  13352  rngressid  13450  ring1  13555  ringressid  13559  subrgsubm  13730  resrhm2b  13745  lssex  13850  cncrng  14057  eltpsg  14208  tg1  14227  cldval  14267  cldss  14273  cldopn  14275  psmetdmdm  14492  dvef  14873  relogef  14999  zabsle1  15115  bj-nn0suc0  15442