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  3072  onsucelsucr  4541  sucunielr  4543  ordsuc  4596  peano2b  4648  xpiindim  4800  fvelrnb  5605  fliftcnv  5839  riotaprop  5898  unielxp  6229  dmtpos  6311  tpossym  6331  ercnv  6610  cnvct  6865  php5dom  6921  3xpfi  6989  recrecnq  7456  1idpr  7654  eqlei2  8116  lem1  8868  eluzfz1  10100  fzpred  10139  uznfz  10172  fz0fzdiffz0  10199  fzctr  10202  flid  10356  flqeqceilz  10392  faclbnd3  10817  bcn1  10832  isfinite4im  10866  leabs  11221  gcd0id  12119  lcmgcdlem  12218  dvdsnprmd  12266  pcprod  12487  fldivp1  12489  intopsn  12953  mgm1  12956  sgrp1  12997  mnd1  13030  mnd1id  13031  grp1  13181  grp1inv  13182  eqger  13297  eqgid  13299  qusghm  13355  rngressid  13453  ring1  13558  ringressid  13562  subrgsubm  13733  resrhm2b  13748  lssex  13853  cncrng  14068  eltpsg  14219  tg1  14238  cldval  14278  cldss  14284  cldopn  14286  psmetdmdm  14503  dvef  14906  relogef  15040  zabsle1  15156  bj-nn0suc0  15512