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  4545  sucunielr  4547  ordsuc  4600  peano2b  4652  xpiindim  4804  fvelrnb  5611  fliftcnv  5845  riotaprop  5904  unielxp  6241  dmtpos  6323  tpossym  6343  ercnv  6622  cnvct  6877  php5dom  6933  3xpfi  7003  recrecnq  7480  1idpr  7678  eqlei2  8140  lem1  8893  eluzfz1  10125  fzpred  10164  uznfz  10197  fz0fzdiffz0  10224  fzctr  10227  flid  10393  flqeqceilz  10429  faclbnd3  10854  bcn1  10869  isfinite4im  10903  leabs  11258  gcd0id  12173  lcmgcdlem  12272  dvdsnprmd  12320  pcprod  12542  fldivp1  12544  intopsn  13071  mgm1  13074  sgrp1  13115  mnd1  13159  mnd1id  13160  grp1  13310  grp1inv  13311  eqger  13432  eqgid  13434  qusghm  13490  rngressid  13588  ring1  13693  ringressid  13697  subrgsubm  13868  resrhm2b  13883  lssex  13988  cncrng  14203  eltpsg  14384  tg1  14403  cldval  14443  cldss  14449  cldopn  14451  psmetdmdm  14668  dvef  15071  relogef  15208  zabsle1  15348  bj-nn0suc0  15704