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  3115  onsucelsucr  4600  sucunielr  4602  ordsuc  4655  peano2b  4707  xpiindim  4859  fununfun  5364  fvelrnb  5683  fliftcnv  5925  riotaprop  5986  unielxp  6326  dmtpos  6408  tpossym  6428  ercnv  6709  cnvct  6970  php5dom  7032  3xpfi  7106  recrecnq  7592  1idpr  7790  eqlei2  8252  lem1  9005  eluzfz1  10239  fzpred  10278  uznfz  10311  fz0fzdiffz0  10338  fzctr  10341  flid  10516  flqeqceilz  10552  faclbnd3  10977  bcn1  10992  isfinite4im  11026  leabs  11601  gcd0id  12516  lcmgcdlem  12615  dvdsnprmd  12663  pcprod  12885  fldivp1  12887  intopsn  13416  mgm1  13419  sgrp1  13460  mnd1  13504  mnd1id  13505  grp1  13655  grp1inv  13656  eqger  13777  eqgid  13779  qusghm  13835  rngressid  13933  ring1  14038  ringressid  14042  subrgsubm  14214  resrhm2b  14229  lssex  14334  cncrng  14549  eltpsg  14730  tg1  14749  cldval  14789  cldss  14795  cldopn  14797  psmetdmdm  15014  dvef  15417  relogef  15554  zabsle1  15694  usgredg2vlem2  16037  wlkprop  16073  wlkvtxiedg  16091  bj-nn0suc0  16396