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  3075  onsucelsucr  4544  sucunielr  4546  ordsuc  4599  peano2b  4651  xpiindim  4803  fvelrnb  5608  fliftcnv  5842  riotaprop  5901  unielxp  6232  dmtpos  6314  tpossym  6334  ercnv  6613  cnvct  6868  php5dom  6924  3xpfi  6994  recrecnq  7461  1idpr  7659  eqlei2  8121  lem1  8874  eluzfz1  10106  fzpred  10145  uznfz  10178  fz0fzdiffz0  10205  fzctr  10208  flid  10374  flqeqceilz  10410  faclbnd3  10835  bcn1  10850  isfinite4im  10884  leabs  11239  gcd0id  12146  lcmgcdlem  12245  dvdsnprmd  12293  pcprod  12515  fldivp1  12517  intopsn  13010  mgm1  13013  sgrp1  13054  mnd1  13087  mnd1id  13088  grp1  13238  grp1inv  13239  eqger  13354  eqgid  13356  qusghm  13412  rngressid  13510  ring1  13615  ringressid  13619  subrgsubm  13790  resrhm2b  13805  lssex  13910  cncrng  14125  eltpsg  14276  tg1  14295  cldval  14335  cldss  14341  cldopn  14343  psmetdmdm  14560  dvef  14963  relogef  15100  zabsle1  15240  bj-nn0suc0  15596