Theorem syl5ibcom 235

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 |- ( ph -> ps )
2		syl5ib.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5ib 234	. 2 |- ( ch -> ( ph -> th ) )
4	3	com12 32	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   <-> wb 196

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

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  biimpcd  239  elrab3t  3362  mob2  3386  rmob  3529  sneqrg  4370  preq1b  4377  disjxun  4651  sotric  5061  sotrieq  5062  iss  5447  poirr2  5520  xp11  5569  nordeq  5742  nsuceq0  5805  suctrOLD  5809  ordequn  5828  tz6.12c  6213  fnbrfvb  6236  foeqcnvco  6555  f1eqcocnv  6556  dfwe2  6981  mpt2sn  7268  tfrlem15  7488  tz7.44-2  7503  tz7.48-1  7538  tz7.49  7540  oawordexr  7636  oewordi  7671  oeeulem  7681  nna0r  7689  nnawordex  7717  nnaordex  7718  oaabs  7724  oaabs2  7725  ectocld  7814  ecoptocl  7837  mapsn  7899  eqeng  7989  difsnen  8042  fopwdom  8068  frfi  8205  elfiun  8336  ordiso  8421  ordtypelem7  8429  wemaplem2  8452  suc11reg  8516  inf3lem6  8530  noinfep  8557  cantnff  8571  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnflem1  8586  cantnf  8590  r111  8638  rankc2  8734  tcrank  8747  cardnueq0  8790  fodomfi2  8883  alephinit  8918  dfac9  8958  dfac12k  8969  cdainf  9014  ackbij1  9060  ackbij2  9065  sornom  9099  fin23lem16  9157  fin23lem21  9161  isf32lem2  9176  fin1a2lem6  9227  itunitc  9243  zorn2lem4  9321  wunr1om  9541  tskr1om  9589  recmulnq  9786  ltexnq  9797  distrlem4pr  9848  1re  10039  0re  10040  0cnALT  10270  mulge0  10546  prodgt0  10868  peano2nn  11032  recnz  11452  zneo  11460  uzn0  11703  xlemul1a  12118  prunioo  12301  flidz  12611  ceilidz  12651  modid2  12697  modmuladdnn0  12714  om2uzrani  12751  uzrdgfni  12757  seqid  12846  seqz  12849  facdiv  13074  facwordi  13076  hashdom  13168  wrdnval  13335  wrdl1s1  13394  sqrmo  13992  fsumf1o  14454  isumltss  14580  supcvg  14588  dvdsnegb  14999  odd2np1lem  15064  odd2np1  15065  ltoddhalfle  15085  halfleoddlt  15086  opoe  15087  omoe  15088  opeo  15089  omeo  15090  bitsuz  15196  bezoutlem4  15259  gcddiv  15268  gcdzeq  15271  dvdssqim  15273  lcmgcdeq  15325  coprmdvds2  15368  rpmul  15373  divgcdcoprmex  15380  cncongr2  15382  dvdsprm  15415  coprm  15423  prmdvdsexp  15427  prmdiv  15490  pythagtriplem19  15538  pc2dvds  15583  pcadd  15593  prmpwdvds  15608  vdwlem11  15695  ramubcl  15722  0ram  15724  mreexexdOLD  16309  posasymb  16952  pleval2  16965  pltval3  16967  plttr  16970  pospo  16973  letsr  17227  intopsn  17253  ismgmid  17264  imasmnd2  17327  isgrpid2  17458  isgrpinv  17472  dfgrp3lem  17513  imasgrp2  17530  orbsta  17746  symgfix2  17836  pmtrfrn  17878  pmtrrn2  17880  odmulg  17973  odmulgeq  17974  gexdvdsi  17998  gexnnod  18003  pgpssslw  18029  sylow2alem1  18032  fislw  18040  lsmss1b  18080  lsmss2b  18082  efgrelexlemb  18163  torsubg  18257  ablfacrplem  18464  pgpfac1lem2  18474  pgpfac1lem3  18476  imasring  18619  dvdsrcl2  18650  dvdsrtr  18652  dvdsrmul1  18653  irredn0  18703  lspsneq0  19012  lmhmima  19047  lspsolv  19143  opsrtoslem2  19485  mpfind  19536  mpfpf1  19715  pf1mpf  19716  xrsdsreclblem  19792  dvdsrzring  19831  prmirredlem  19841  znunit  19912  pjdm2  20055  obselocv  20072  lindfrn  20160  cpmadugsumlemF  20681  baspartn  20758  bastop  20785  iscld3  20868  isopn3  20870  iscldtop  20899  ordtrest2lem  21007  2ndcredom  21253  2ndc1stc  21254  2ndcrest  21257  2ndcdisj  21259  2ndcsep  21262  kgenidm  21350  dfac14  21421  tx2ndc  21454  kqreglem1  21544  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  flimtopon  21774  fclstopon  21816  xrsmopn  22615  icccmplem2  22626  reconnlem1  22629  iccpnfcnv  22743  cphsqrtcl2  22986  ivthlem3  23222  ivthicc  23227  ovolctb  23258  ioombl  23333  itgabs  23601  itgsplitioo  23604  dvlip  23756  c1liplem1  23759  c1lip1  23760  dvgt0lem1  23765  dvivthlem2  23772  dvne0  23774  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  dvcvx  23783  itgsubstlem  23811  mdegnn0cl  23831  ig1peu  23931  elply2  23952  plypf1  23968  dgreq0  24021  aannenlem3  24085  abelthlem2  24186  lognegb  24336  eflogeq  24348  efopn  24404  cxpge0  24429  cxplea  24442  cxple2  24443  cxpcn3lem  24488  cxpaddlelem  24492  cxpaddle  24493  cxpeq  24498  asinsinb  24624  acoscosb  24625  atantanb  24651  leibpilem1  24667  wilthlem2  24795  sqf11  24865  sqff1o  24908  ppiublem1  24927  lgsdir  25057  lgsne0  25060  lgsquadlem3  25107  2sqblem  25156  dchrisum0flblem1  25197  ostth3  25327  ostth  25328  colinearalg  25790  axcontlem5  25848  axcontlem9  25852  uhgrn0  25962  upgrfn  25982  umgrfn  25994  uvtxanbgrvtx  26293  vtxduhgr0nedg  26388  pthdivtx  26625  iswwlksnx  26731  clwlksf1clwwlklem1  26965  eupth2lem2  27079  eupth2lem3lem6  27093  htthlem  27774  pjpreeq  28257  h1dn0  28411  spansneleqi  28428  rnbra  28966  dfpjop  29041  elpjrn  29049  stm1i  29102  mdbr2  29155  mdsl2i  29181  sumdmdlem  29277  dmdbr6ati  29282  ordtrest2NEWlem  29968  xrge0iifcnv  29979  eulerpartlemb  30430  erdszelem8  31180  cvmlift3lem4  31304  cvmlift3lem5  31305  mrsub0  31413  mrsubccat  31415  mrsubcn  31416  msubrn  31426  msrid  31442  elmthm  31473  dvdspw  31636  dfon2lem9  31696  poseq  31750  noseponlem  31817  nodenselem4  31837  nodenselem5  31838  nodenselem7  31840  nodenselem8  31841  nolt02o  31845  nosupbnd2lem1  31861  noetalem3  31865  slerec  31923  btwnconn1lem11  32204  broutsideof2  32229  opnbnd  32320  tailfb  32372  bj-ismooredr2  33065  fin2so  33396  poimirlem9  33418  poimirlem17  33426  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  itgabsnc  33479  ftc2nc  33494  sdclem2  33538  subspopn  33548  equivtotbnd  33577  rngosn3  33723  igenval2  33865  isfldidl  33867  relcnveq3  34092  ecex2  34100  iss2  34112  lshpinN  34276  lsatcv0eq  34334  lsatcv1  34335  cvrnbtwn3  34563  cvrnbtwn4  34566  cvrcmp  34570  atnlt  34600  cvlexchb1  34617  2llnne2N  34694  atcvr0eq  34712  lnnat  34713  cvrat4  34729  ps-1  34763  3at  34776  llncmp  34808  llnnlt  34809  llncvrlpln2  34843  llncvrlpln  34844  lplncmp  34848  lplnnlt  34851  lplncvrlvol2  34901  lplncvrlvol  34902  lvolcmp  34903  lvolnltN  34904  dalempnes  34937  dalemqnet  34938  dalem-cly  34957  dalem44  35002  lncmp  35069  cdlemblem  35079  llnexch2N  35156  osumcllem4N  35245  pexmidlem1N  35256  lhp2atnle  35319  cdleme11dN  35549  cdleme20k  35607  cdleme21at  35616  cdleme21ct  35617  cdleme32e  35733  cdleme35f  35742  tendoex  36263  dochexmidlem1  36749  lcfrlem9  36839  mapd1o  36937  mapdindp3  37011  ismrc  37264  pellexlem1  37393  aomclem4  37627  dfac21  37636  lsmfgcl  37644  lmhmfgima  37654  dfacbasgrp  37678  hbtlem6  37699  fiuneneq  37775  mapsnd  39388  stoweidlem27  40244  stoweidlem29  40246  iccpartrn  41366  prmdvdsfmtnof1lem2  41497  mod42tp1mod8  41519  assintopass  41850