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  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  7478  1idpr  7676  eqlei2  8138  lem1  8891  eluzfz1  10123  fzpred  10162  uznfz  10195  fz0fzdiffz0  10222  fzctr  10225  flid  10391  flqeqceilz  10427  faclbnd3  10852  bcn1  10867  isfinite4im  10901  leabs  11256  gcd0id  12171  lcmgcdlem  12270  dvdsnprmd  12318  pcprod  12540  fldivp1  12542  intopsn  13069  mgm1  13072  sgrp1  13113  mnd1  13157  mnd1id  13158  grp1  13308  grp1inv  13309  eqger  13430  eqgid  13432  qusghm  13488  rngressid  13586  ring1  13691  ringressid  13695  subrgsubm  13866  resrhm2b  13881  lssex  13986  cncrng  14201  eltpsg  14360  tg1  14379  cldval  14419  cldss  14425  cldopn  14427  psmetdmdm  14644  dvef  15047  relogef  15184  zabsle1  15324  bj-nn0suc0  15680