Theorem syl5ibcom 234

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

Hypotheses

Ref	Expression
syl5ib.1	⊢ (𝜑 → 𝜓)
syl5ib.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibcom	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5ib.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5ib 233	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  biimpcd  238  elrab3t  3330  mob2  3353  rmob  3495  sneqrg  4310  preq1b  4317  disjxun  4581  sotric  4985  sotrieq  4986  iss  5367  poirr2  5439  xp11  5488  nordeq  5659  nsuceq0  5722  suctrOLD  5726  ordequn  5745  tz6.12c  6123  fnbrfvb  6146  foeqcnvco  6455  f1eqcocnv  6456  dfwe2  6873  mpt2sn  7155  tfrlem15  7375  tz7.44-2  7390  tz7.48-1  7425  tz7.49  7427  oawordexr  7523  oewordi  7558  oeeulem  7568  nna0r  7576  nnawordex  7604  nnaordex  7605  oaabs  7611  oaabs2  7612  ectocld  7701  ecoptocl  7724  mapsn  7785  eqeng  7875  difsnen  7927  fopwdom  7953  frfi  8090  elfiun  8219  ordiso  8304  ordtypelem7  8312  wemaplem2  8335  suc11reg  8399  inf3lem6  8413  noinfep  8440  cantnff  8454  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnflem1  8469  cantnf  8473  r111  8521  rankc2  8617  tcrank  8630  cardnueq0  8673  fodomfi2  8766  alephinit  8801  dfac9  8841  dfac12k  8852  cdainf  8897  ackbij1  8943  ackbij2  8948  sornom  8982  fin23lem16  9040  fin23lem21  9044  isf32lem2  9059  fin1a2lem6  9110  itunitc  9126  zorn2lem4  9204  wunr1om  9420  tskr1om  9468  recmulnq  9665  ltexnq  9676  distrlem4pr  9727  1re  9918  0re  9919  0cnALT  10149  mulge0  10425  prodgt0  10747  peano2nn  10909  recnz  11328  zneo  11336  uzn0  11579  xlemul1a  11990  prunioo  12172  flidz  12473  ceilidz  12513  modid2  12559  modmuladdnn0  12576  om2uzrani  12613  uzrdgfni  12619  seqid  12708  seqz  12711  facdiv  12936  facwordi  12938  hashdom  13029  wrdnval  13190  wrdl1s1  13247  sqrmo  13840  fsumf1o  14301  isumltss  14419  supcvg  14427  dvdsnegb  14837  odd2np1lem  14902  odd2np1  14903  ltoddhalfle  14923  halfleoddlt  14924  opoe  14925  omoe  14926  opeo  14927  omeo  14928  bitsuz  15034  bezoutlem4  15097  gcddiv  15106  gcdzeq  15109  dvdssqim  15111  lcmgcdeq  15163  coprmdvds2  15206  rpmul  15211  divgcdcoprmex  15218  cncongr2  15220  dvdsprm  15253  coprm  15261  prmdvdsexp  15265  prmdiv  15328  pythagtriplem19  15376  pc2dvds  15421  pcadd  15431  prmpwdvds  15446  vdwlem11  15533  ramubcl  15560  0ram  15562  mreexexdOLD  16132  posasymb  16775  pleval2  16788  pltval3  16790  plttr  16793  pospo  16796  letsr  17050  intopsn  17076  ismgmid  17087  imasmnd2  17150  isgrpid2  17281  isgrpinv  17295  dfgrp3lem  17336  imasgrp2  17353  orbsta  17569  symgfix2  17659  pmtrfrn  17701  pmtrrn2  17703  odmulg  17796  odmulgeq  17797  gexdvdsi  17821  gexnnod  17826  pgpssslw  17852  sylow2alem1  17855  fislw  17863  lsmss1b  17903  lsmss2b  17905  efgrelexlemb  17986  torsubg  18080  ablfacrplem  18287  pgpfac1lem2  18297  pgpfac1lem3  18299  imasring  18442  dvdsrcl2  18473  dvdsrtr  18475  dvdsrmul1  18476  irredn0  18526  lspsneq0  18833  lmhmima  18868  lspsolv  18964  opsrtoslem2  19306  mpfind  19357  mpfpf1  19536  pf1mpf  19537  xrsdsreclblem  19611  dvdsrzring  19650  prmirredlem  19660  znunit  19731  pjdm2  19874  obselocv  19891  lindfrn  19979  cpmadugsumlemF  20500  baspartn  20569  bastop  20596  iscld3  20678  isopn3  20680  iscldtop  20709  ordtrest2lem  20817  2ndcredom  21063  2ndc1stc  21064  2ndcrest  21067  2ndcdisj  21069  2ndcsep  21072  kgenidm  21160  dfac14  21231  tx2ndc  21264  kqreglem1  21354  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  flimtopon  21584  fclstopon  21626  xrsmopn  22423  icccmplem2  22434  reconnlem1  22437  iccpnfcnv  22551  cphsqrtcl2  22794  ivthlem3  23029  ivthicc  23034  ovolctb  23065  ioombl  23140  itgabs  23407  itgsplitioo  23410  dvlip  23560  c1liplem1  23563  c1lip1  23564  dvgt0lem1  23569  dvivthlem2  23576  dvne0  23578  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  dvcvx  23587  itgsubstlem  23615  mdegnn0cl  23635  ig1peu  23735  elply2  23756  plypf1  23772  dgreq0  23825  aannenlem3  23889  abelthlem2  23990  lognegb  24140  eflogeq  24152  efopn  24204  cxpge0  24229  cxplea  24242  cxple2  24243  cxpcn3lem  24288  cxpaddlelem  24292  cxpaddle  24293  cxpeq  24298  asinsinb  24424  acoscosb  24425  atantanb  24451  leibpilem1  24467  wilthlem2  24595  sqf11  24665  sqff1o  24708  ppiublem1  24727  lgsdir  24857  lgsne0  24860  lgsquadlem3  24907  2sqblem  24956  dchrisum0flblem1  24997  ostth3  25127  ostth  25128  colinearalg  25590  axcontlem5  25648  axcontlem9  25652  uhgrn0  25733  upgrfn  25754  umgrfn  25765  umgraf  25847  uslgraf1oedg  25888  nbgrassvwo  25966  usgrcyclnl1  26168  nvnencycllem  26171  clwwlknprop  26300  clwlkf1clwwlklem1  26373  usg2wlkonot  26410  usg2wotspth  26411  eupath2lem2  26505  eupath2lem3  26506  htthlem  27158  pjpreeq  27641  h1dn0  27795  spansneleqi  27812  rnbra  28350  dfpjop  28425  elpjrn  28433  stm1i  28486  mdbr2  28539  mdsl2i  28565  sumdmdlem  28661  dmdbr6ati  28666  ordtrest2NEWlem  29296  xrge0iifcnv  29307  eulerpartlemb  29757  erdszelem8  30434  cvmlift3lem4  30558  cvmlift3lem5  30559  mrsub0  30667  mrsubccat  30669  mrsubcn  30670  msubrn  30680  msrid  30696  elmthm  30727  dvdspw  30889  dfon2lem9  30940  poseq  30994  noseponlem  31065  nodenselem3  31082  nodenselem5  31084  nodenselem8  31087  nofulllem5  31105  btwnconn1lem11  31374  broutsideof2  31399  opnbnd  31490  tailfb  31542  fin2so  32566  poimirlem9  32588  poimirlem17  32596  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  itgabsnc  32649  ftc2nc  32664  sdclem2  32708  subspopn  32718  equivtotbnd  32747  rngosn3  32893  igenval2  33035  isfldidl  33037  lshpinN  33294  lsatcv0eq  33352  lsatcv1  33353  cvrnbtwn3  33581  cvrnbtwn4  33584  cvrcmp  33588  atnlt  33618  cvlexchb1  33635  2llnne2N  33712  atcvr0eq  33730  lnnat  33731  cvrat4  33747  ps-1  33781  3at  33794  llncmp  33826  llnnlt  33827  llncvrlpln2  33861  llncvrlpln  33862  lplncmp  33866  lplnnlt  33869  lplncvrlvol2  33919  lplncvrlvol  33920  lvolcmp  33921  lvolnltN  33922  dalempnes  33955  dalemqnet  33956  dalem-cly  33975  dalem44  34020  lncmp  34087  cdlemblem  34097  llnexch2N  34174  osumcllem4N  34263  pexmidlem1N  34274  lhp2atnle  34337  cdleme11dN  34567  cdleme20k  34625  cdleme21at  34634  cdleme21ct  34635  cdleme32e  34751  cdleme35f  34760  tendoex  35281  dochexmidlem1  35767  lcfrlem9  35857  mapd1o  35955  mapdindp3  36029  ismrc  36282  pellexlem1  36411  aomclem4  36645  dfac21  36654  lsmfgcl  36662  lmhmfgima  36672  dfacbasgrp  36697  hbtlem6  36718  fiuneneq  36794  mapsnd  38383  stoweidlem27  38920  stoweidlem29  38922  iccpartrn  39968  prmdvdsfmtnof1lem2  40035  mod42tp1mod8  40057  uspgrf1oedg  40403  uvtxanbgrvtx  40619  vtxduhgr0nedg  40707  pthdivtx  40935  iswwlksnx  41042  clwlksf1clwwlklem1  41272  eupth2lem2  41387  eupth2lem3lem6  41401  assintopass  41640