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  3050  onsucelsucr  4509  sucunielr  4511  ordsuc  4564  peano2b  4616  xpiindim  4766  fvelrnb  5565  fliftcnv  5798  riotaprop  5856  unielxp  6177  dmtpos  6259  tpossym  6279  ercnv  6558  cnvct  6811  php5dom  6865  3xpfi  6932  recrecnq  7395  1idpr  7593  eqlei2  8054  lem1  8806  eluzfz1  10033  fzpred  10072  uznfz  10105  fz0fzdiffz0  10132  fzctr  10135  flid  10286  flqeqceilz  10320  faclbnd3  10725  bcn1  10740  isfinite4im  10774  leabs  11085  gcd0id  11982  lcmgcdlem  12079  dvdsnprmd  12127  pcprod  12346  fldivp1  12348  intopsn  12791  mgm1  12794  sgrp1  12821  mnd1  12852  mnd1id  12853  grp1  12981  grp1inv  12982  eqger  13088  eqgid  13090  ring1  13241  ringressid  13243  subrgsubm  13360  cncrng  13502  eltpsg  13579  tg1  13598  cldval  13638  cldss  13644  cldopn  13646  psmetdmdm  13863  dvef  14227  relogef  14324  zabsle1  14439  bj-nn0suc0  14741