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	|- ( ps -> ph )
mpancom.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpancom	|- ( ps -> ch )

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 |- ( ps -> ph )
2		id 19	. 2 |- ( ps -> ps )
3		mpancom.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	1, 2, 3	syl2anc 411	1 |- ( ps -> ch )

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  4528  sucunielr  4530  ordsuc  4583  peano2b  4635  xpiindim  4785  fvelrnb  5587  fliftcnv  5820  riotaprop  5879  unielxp  6203  dmtpos  6285  tpossym  6305  ercnv  6584  cnvct  6839  php5dom  6895  3xpfi  6963  recrecnq  7428  1idpr  7626  eqlei2  8087  lem1  8839  eluzfz1  10067  fzpred  10106  uznfz  10139  fz0fzdiffz0  10166  fzctr  10169  flid  10321  flqeqceilz  10355  faclbnd3  10764  bcn1  10779  isfinite4im  10813  leabs  11124  gcd0id  12021  lcmgcdlem  12120  dvdsnprmd  12168  pcprod  12389  fldivp1  12391  intopsn  12854  mgm1  12857  sgrp1  12897  mnd1  12930  mnd1id  12931  grp1  13073  grp1inv  13074  eqger  13188  eqgid  13190  qusghm  13246  rngressid  13333  ring1  13436  ringressid  13438  subrgsubm  13606  lssex  13695  cncrng  13897  eltpsg  14025  tg1  14044  cldval  14084  cldss  14090  cldopn  14092  psmetdmdm  14309  dvef  14673  relogef  14770  zabsle1  14886  bj-nn0suc0  15188