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  3063  onsucelsucr  4525  sucunielr  4527  ordsuc  4580  peano2b  4632  xpiindim  4782  fvelrnb  5583  fliftcnv  5816  riotaprop  5874  unielxp  6198  dmtpos  6280  tpossym  6300  ercnv  6579  cnvct  6834  php5dom  6890  3xpfi  6958  recrecnq  7422  1idpr  7620  eqlei2  8081  lem1  8833  eluzfz1  10060  fzpred  10099  uznfz  10132  fz0fzdiffz0  10159  fzctr  10162  flid  10314  flqeqceilz  10348  faclbnd3  10754  bcn1  10769  isfinite4im  10803  leabs  11114  gcd0id  12011  lcmgcdlem  12108  dvdsnprmd  12156  pcprod  12377  fldivp1  12379  intopsn  12840  mgm1  12843  sgrp1  12871  mnd1  12904  mnd1id  12905  grp1  13047  grp1inv  13048  eqger  13160  eqgid  13162  qusghm  13218  rngressid  13305  ring1  13408  ringressid  13410  subrgsubm  13578  lssex  13667  cncrng  13869  eltpsg  13992  tg1  14011  cldval  14051  cldss  14057  cldopn  14059  psmetdmdm  14276  dvef  14640  relogef  14737  zabsle1  14853  bj-nn0suc0  15155