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  3115  onsucelsucr  4597  sucunielr  4599  ordsuc  4652  peano2b  4704  xpiindim  4856  fununfun  5360  fvelrnb  5674  fliftcnv  5912  riotaprop  5973  unielxp  6310  dmtpos  6392  tpossym  6412  ercnv  6691  cnvct  6952  php5dom  7012  3xpfi  7083  recrecnq  7569  1idpr  7767  eqlei2  8229  lem1  8982  eluzfz1  10215  fzpred  10254  uznfz  10287  fz0fzdiffz0  10314  fzctr  10317  flid  10491  flqeqceilz  10527  faclbnd3  10952  bcn1  10967  isfinite4im  11001  leabs  11571  gcd0id  12486  lcmgcdlem  12585  dvdsnprmd  12633  pcprod  12855  fldivp1  12857  intopsn  13386  mgm1  13389  sgrp1  13430  mnd1  13474  mnd1id  13475  grp1  13625  grp1inv  13626  eqger  13747  eqgid  13749  qusghm  13805  rngressid  13903  ring1  14008  ringressid  14012  subrgsubm  14183  resrhm2b  14198  lssex  14303  cncrng  14518  eltpsg  14699  tg1  14718  cldval  14758  cldss  14764  cldopn  14766  psmetdmdm  14983  dvef  15386  relogef  15523  zabsle1  15663  usgredg2vlem2  16006  bj-nn0suc0  16243