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  3084  onsucelsucr  4557  sucunielr  4559  ordsuc  4612  peano2b  4664  xpiindim  4816  fununfun  5318  fvelrnb  5628  fliftcnv  5866  riotaprop  5925  unielxp  6262  dmtpos  6344  tpossym  6364  ercnv  6643  cnvct  6903  php5dom  6962  3xpfi  7032  recrecnq  7509  1idpr  7707  eqlei2  8169  lem1  8922  eluzfz1  10155  fzpred  10194  uznfz  10227  fz0fzdiffz0  10254  fzctr  10257  flid  10429  flqeqceilz  10465  faclbnd3  10890  bcn1  10905  isfinite4im  10939  leabs  11418  gcd0id  12333  lcmgcdlem  12432  dvdsnprmd  12480  pcprod  12702  fldivp1  12704  intopsn  13232  mgm1  13235  sgrp1  13276  mnd1  13320  mnd1id  13321  grp1  13471  grp1inv  13472  eqger  13593  eqgid  13595  qusghm  13651  rngressid  13749  ring1  13854  ringressid  13858  subrgsubm  14029  resrhm2b  14044  lssex  14149  cncrng  14364  eltpsg  14545  tg1  14564  cldval  14604  cldss  14610  cldopn  14612  psmetdmdm  14829  dvef  15232  relogef  15369  zabsle1  15509  bj-nn0suc0  15923