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  3086  onsucelsucr  4561  sucunielr  4563  ordsuc  4616  peano2b  4668  xpiindim  4820  fununfun  5323  fvelrnb  5636  fliftcnv  5874  riotaprop  5933  unielxp  6270  dmtpos  6352  tpossym  6372  ercnv  6651  cnvct  6912  php5dom  6972  3xpfi  7042  recrecnq  7520  1idpr  7718  eqlei2  8180  lem1  8933  eluzfz1  10166  fzpred  10205  uznfz  10238  fz0fzdiffz0  10265  fzctr  10268  flid  10440  flqeqceilz  10476  faclbnd3  10901  bcn1  10916  isfinite4im  10950  leabs  11435  gcd0id  12350  lcmgcdlem  12449  dvdsnprmd  12497  pcprod  12719  fldivp1  12721  intopsn  13249  mgm1  13252  sgrp1  13293  mnd1  13337  mnd1id  13338  grp1  13488  grp1inv  13489  eqger  13610  eqgid  13612  qusghm  13668  rngressid  13766  ring1  13871  ringressid  13875  subrgsubm  14046  resrhm2b  14061  lssex  14166  cncrng  14381  eltpsg  14562  tg1  14581  cldval  14621  cldss  14627  cldopn  14629  psmetdmdm  14846  dvef  15249  relogef  15386  zabsle1  15526  bj-nn0suc0  16000