Theorem syl5com 28

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)

Hypotheses

Ref	Expression
syl5com.1	|- ( ph -> ps )
syl5com.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5com	|- ( ph -> ( ch -> th ) )

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 |- ( ph -> ps )
2	1	a1d 23	. 2 |- ( ph -> ( ch -> ps ) )
3		syl5com.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	sylcom 27	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4

This theorem is referenced by:  com12  29  syl5  30  ax10lem2  1989  ax10  1991  ax16i  2095  ceqsalg  2940  cgsexg  2947  cgsex2g  2948  cgsex4g  2949  spc2egv  2998  spc3egv  3000  disjne  3633  uneqdifeq  3676  triun  4275  ordelord  4563  sucssel  4633  ordsuc  4753  tfi  4792  relresfld  5355  relcoi1  5357  unixpid  5363  fvimacnv  5804  fornex  5929  f1dmex  5930  tz7.49  6661  oeworde  6795  undifixp  7057  dom2d  7107  2pwuninel  7221  findcard  7306  fisupg  7314  dffi3  7394  noinfep  7570  cantnflem2  7602  tcmin  7636  rankr1ag  7684  rankpwi  7705  rankelb  7706  rankunb  7732  rankxpsuc  7762  alephordi  7911  alephsucdom  7916  alephinit  7932  dfac9  7972  ackbij2lem4  8078  cff1  8094  cfslbn  8103  cfcoflem  8108  cfcof  8110  infpssrlem5  8143  isfin7-2  8232  acncc  8276  domtriomlem  8278  axdc3lem2  8287  ttukeylem1  8345  iundom2g  8371  wunex2  8569  grupr  8628  gruiun  8630  eltskm  8674  nqereu  8762  addcanpr  8879  axpre-sup  9000  nneo  10309  zeo2  10312  xrub  10846  uznfz  11085  facndiv  11534  hashf1rn  11591  hashgt12el2  11638  hash2prde  11643  brfi1uzind  11670  fsumcom2  12513  incexclem  12571  isumrpcl  12578  ndvdssub  12882  eucalglt  13031  prmind2  13045  coprm  13055  prmdiveq  13130  drsdir  14347  lubid  14394  istos  14419  latlem  14432  tsrlin  14606  dirge  14637  mhmlin  14700  issubg2  14914  nsgbi  14926  sylow2a  15208  issubrg2  15843  abvmul  15872  abvtri  15873  lmodlema  15910  lspsnel6  16025  lmhmlin  16066  lbsind  16107  cygth  16807  ipcj  16820  obsip  16903  inopn  16927  basis1  16970  tgss  16988  tgcl  16989  elcls3  17102  neindisj2  17142  cnpco  17285  cncls  17292  1stcelcls  17477  txkgen  17637  qtoptop2  17684  nrmr0reg  17734  fbasssin  17821  fbfinnfr  17826  fbunfip  17854  filufint  17905  uffix  17906  ufinffr  17914  ufilen  17915  fmfnfmlem1  17939  flftg  17981  alexsubALT  18035  xmeteq0  18321  blssexps  18409  blssex  18410  mopni3  18477  neibl  18484  metss  18491  metcnp3  18523  nmvs  18665  reperflem  18802  iccntr  18805  reconnlem2  18811  lebnumlem3  18941  caubl  19213  bcthlem5  19234  ovolunlem1  19346  voliunlem1  19397  volsuplem  19402  ellimc3  19719  lhop1lem  19850  ulmss  20266  dchrisumlema  21135  usgrarnedg  21357  usgrafisbase  21381  sizeusglecusglem1  21446  uvtxisvtx  21452  usgrnloop  21516  usgrcyclnl2  21581  eupatrl  21643  ablocom  21826  rngodm1dm2  21959  rngoueqz  21971  zerdivemp1  21975  rngoridfz  21976  ubthlem1  22325  shaddcl  22672  shmulcl  22673  shmulclOLD  22674  spansnss2  23030  cnopc  23369  cnfnc  23386  adj1  23389  pjorthcoi  23625  stj  23691  mdsl1i  23777  chirredlem1  23846  mdsymlem5  23863  cdj3lem2b  23893  pconcn  24864  cvmlift2lem1  24942  relin01  25147  fprodss  25227  fprodcom2  25261  dfon2lem6  25358  wfrlem4  25473  wfrlem10  25479  frrlem4  25498  nofv  25525  nodenselem4  25552  waj-ax  26068  lukshef-ax2  26069  ontgval  26085  nn0prpw  26216  heiborlem1  26410  zerdivemp1x  26461  isdrngo3  26465  0rngo  26527  pridl  26537  ispridlc  26570  isdmn3  26574  dmnnzd  26575  dfac21  27032  lindsss  27162  2f1fvneq  27958  imarnf1pr  27965  ssfzo12  27990  swrdswrd  28011  swrdccatin12lem3  28024  swrdccatin12  28026  usgra2wlkspthlem1  28036  usgfiregdegfi  28091  2pthfrgra  28115  3cyclfrgrarn2  28118  frgrancvvdeqlemB  28141  frgrawopreg1  28153  frgrawopreg2  28154  frgraeu  28157  eexinst11  28322  a9e2eq  28355  e222  28446  e111  28484  eel12131  28530  e333  28554  ax16iNEW7  29255  lshpcmp  29471  omllaw  29726  dochexmidlem7  31949  lspindp5  32253

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8