Theorem syl5ibcom 248

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		imbitrid.1	. . 3 ⊢ (𝜑 → 𝜓)
2		imbitrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	imbitrid 247	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 33	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimpcd  252  elrab3t  3650  mob2  3679  rmob  3844  sneqrg  4805  preq1b  4812  prel12g  4830  disjxun  5108  sotric  5601  sotrieq  5602  iss  6039  poirr2  6126  xp11  6175  nordeq  6381  nsuceq0  6448  ordequn  6468  fnbrfvb  6933  2f1fvneq  7260  foeqcnvco  7300  f1eqcocnv  7301  dfwe2  7774  releldmdifi  8043  mposn  8099  poxp2  8140  poxp3  8147  poseq  8155  tfrlem15  8380  tz7.44-2  8395  tz7.48-1  8431  tz7.49  8433  oawordexr  8542  oewordi  8578  oeeulem  8588  nna0r  8596  nnawordex  8624  nnaordex  8625  nnaordex2  8626  oaabs  8635  oaabs2  8636  eldifsucnn  8651  elecex  8746  ectocld  8781  ecoptocl  8806  mapsnd  8885  eqeng  8984  difsnen  9048  fopwdom  9074  nneneq  9191  frfi  9246  elfiun  9391  ordiso  9479  ordtypelem7  9487  wemaplem2  9510  suc11reg  9589  inf3lem6  9603  noinfep  9630  cantnff  9644  cantnfp1lem2  9649  cantnfp1lem3  9650  cantnflem1  9659  cantnf  9663  ttrcltr  9686  r111  9748  rankc2  9844  tcrank  9857  cardnueq0  9951  fodomfi2  10045  alephinit  10080  dfac9  10121  dfac12k  10132  djuinf  10173  ackbij1  10221  ackbij2  10226  sornom  10262  fin23lem16  10320  fin23lem21  10324  isf32lem2  10339  fin1a2lem6  10390  itunitc  10406  zorn2lem4  10484  wunr1om  10705  tskr1om  10753  recmulnq  10950  ltexnq  10961  distrlem4pr  11012  1re  11209  0re  11211  0cnALT  11446  0cnALT2  11447  mulge0  11733  prodgt0  12063  peano2nn  12246  recnz  12672  zneo  12680  uzn0  12880  xlemul1a  13315  prunioo  13509  flidz  13845  ceilidz  13887  modid2  13933  modmuladdnn0  13953  om2uzrani  13990  uzrdgfni  13996  seqid  14085  seqz  14088  facdiv  14325  facwordi  14327  hashdom  14417  wrdnval  14584  wrdnfi  14587  wrdl1s1  14654  sqrmo  15304  fsumf1o  15776  isumltss  15904  supcvg  15912  dvdsnegb  16332  dvdsexp2im  16386  odd2np1lem  16399  odd2np1  16400  ltoddhalfle  16420  halfleoddlt  16421  opoe  16422  omoe  16423  opeo  16424  omeo  16425  bitsuz  16533  bezoutlem4  16601  gcddiv  16610  gcdzeq  16611  dvdssqim  16613  dvdsexpim  16614  lcmgcdeq  16671  coprmdvds2  16713  rpmul  16718  divgcdcoprmex  16725  cncongr2  16727  dvdsprm  16763  coprm  16771  prmdvdsexp  16775  prmdiv  16845  pythagtriplem19  16894  pc2dvds  16940  pcadd  16950  prmpwdvds  16965  vdwlem11  17052  ramubcl  17079  0ram  17081  posasymb  18376  pleval2  18392  pltval3  18394  plttr  18397  pospo  18400  letsr  18650  intopsn  18713  ismgmid  18724  imasmnd2  18833  isgrpid2  19044  isgrpinv  19061  dfgrp3lem  19105  imasgrp2  19122  orbsta  19384  symgfix2  19487  pmtrfrn  19529  pmtrrn2  19531  odmulg  19627  odmulgeq  19628  gexdvdsi  19654  gexnnod  19659  pgpssslw  19685  sylow2alem1  19688  fislw  19696  lsmss1b  19737  lsmss2b  19739  efgrelexlemb  19821  torsubg  19925  ablfacrplem  20138  pgpfac1lem2  20148  pgpfac1lem3  20150  ablsimpnosubgd  20177  imasrng  20256  imasring  20413  dvdsrcl2  20449  dvdsrtr  20451  dvdsrmul1  20452  irredn0  20506  lspsneq0  21114  lmhmima  21149  lspsolv  21248  rspprop  21351  xrsdsreclblem  21544  dvdsrzring  21592  prmirredlem  21603  znunit  21694  pjdm2  21842  obselocv  21859  lindfrn  21952  opsrtoslem2  22188  mpfind  22247  psdmul  22310  mpfpf1  22492  pf1mpf  22493  cpmadugsumlemF  23014  baspartn  23092  bastop  23119  iscld3  23202  isopn3  23204  iscldtop  23233  ordtrest2lem  23341  2ndcredom  23588  2ndc1stc  23589  2ndcrest  23592  2ndcdisj  23594  2ndcsep  23597  kgenidm  23685  dfac14  23756  tx2ndc  23789  kqreglem1  23879  rnelfm  24091  fmfnfmlem2  24093  fmfnfmlem4  24095  fmfnfm  24096  flimtopon  24108  fclstopon  24150  xrsmopn  24951  icccmplem2  24962  reconnlem1  24965  iccpnfcnv  25084  cphsqrtcl2  25326  ivthlem3  25593  ivthicc  25598  ovolctb  25630  ioombl  25705  itgabs  25975  itgsplitioo  25978  dvlip  26133  c1liplem1  26136  c1lip1  26137  dvgt0lem1  26142  dvivthlem2  26149  dvne0  26151  lhop1lem  26153  lhop1  26154  lhop2  26155  lhop  26156  dvcvx  26160  itgsubstlem  26188  mdegnn0cl  26209  ig1peu  26313  elply2  26334  plypf1  26350  dgreq0  26403  aannenlem3  26474  abelthlem2  26576  lognegb  26736  eflogeq  26748  efopn  26804  cxpge0  26829  cxplea  26842  cxple2  26843  cxpcn3lem  26893  cxpaddlelem  26897  cxpaddle  26898  cxpeq  26903  asinsinb  27043  acoscosb  27044  atantanb  27070  wilthlem2  27214  sqf11  27284  sqff1o  27327  ppiublem1  27347  lgsdir  27477  lgsne0  27480  lgsquadlem3  27527  2sqblem  27576  dchrisum0flblem1  27653  ostth3  27783  ostth  27784  noseponlem  27809  nodenselem4  27832  nodenselem5  27833  nodenselem7  27835  nodenselem8  27836  nolt02o  27840  nogt01o  27841  nosupbnd2lem1  27860  noetasuplem4  27881  lesrec  27973  madebdayim  28062  negsproplem2  28203  negsunif  28229  negleft  28232  negright  28233  lemuls1ad  28356  precsexlem6  28386  precsexlem7  28387  noseqp1  28465  om2noseqlt  28473  noseqrdgfn  28480  bdayn0sf1o  28544  dfnns2  28546  bdayfinbndlem1  28641  colinearalg  29241  axcontlem5  29299  axcontlem9  29303  uhgrn0  29398  upgrfn  29418  umgrfn  29430  uvtxnbgrvtx  29724  vtxduhgr0nedg  29823  pthdivtx  30057  iswwlksnx  30170  wpthswwlks2on  30294  clwwlkn  30358  clwwlknonwwlknonb  30438  eupth2lem2  30551  eupth2lem3lem6  30565  htthlem  31250  pjpreeq  31731  h1dn0  31885  spansneleqi  31902  rnbra  32440  dfpjop  32515  elpjrn  32523  stm1i  32576  mdbr2  32629  mdsl2i  32655  sumdmdlem  32751  dmdbr6ati  32756  ordtrest2NEWlem  34293  xrge0iifcnv  34304  eulerpartlemb  34739  onvf1odlem4  35571  erdszelem8  35671  cvmlift3lem4  35795  cvmlift3lem5  35796  fmlasucdisj  35872  mrsub0  35989  mrsubccat  35991  mrsubcn  35992  msubrn  36002  msrid  36018  elmthm  36049  dfon2lem9  36262  btwnconn1lem11  36570  broutsideof2  36595  opnbnd  36817  tailfb  36869  tr0elw  36976  tr0el  36977  bj-ideqg1  37789  fin2so  38239  lindsadd  38245  poimirlem9  38261  poimirlem17  38269  poimirlem26  38278  poimirlem27  38279  poimirlem31  38283  itgabsnc  38321  ftc2nc  38334  sdclem2  38374  subspopn  38384  equivtotbnd  38410  rngosn3  38556  igenval2  38698  isfldidl  38700  relcnveq3  38957  iss2  38974  elrelscnveq3  39257  lshpinN  39744  lsatcv0eq  39802  lsatcv1  39803  cvrnbtwn3  40031  cvrnbtwn4  40034  cvrcmp  40038  atnlt  40068  cvlexchb1  40085  2llnne2N  40163  atcvr0eq  40181  lnnat  40182  cvrat4  40198  ps-1  40232  3at  40245  llncmp  40277  llnnlt  40278  llncvrlpln2  40312  llncvrlpln  40313  lplncmp  40317  lplnnlt  40320  lplncvrlvol2  40370  lplncvrlvol  40371  lvolcmp  40372  lvolnltN  40373  dalempnes  40406  dalemqnet  40407  dalem-cly  40426  dalem44  40471  lncmp  40538  cdlemblem  40548  llnexch2N  40625  osumcllem4N  40714  pexmidlem1N  40725  lhp2atnle  40788  cdleme11dN  41017  cdleme20k  41074  cdleme21at  41083  cdleme21ct  41084  cdleme32e  41200  cdleme35f  41209  tendoex  41730  dochexmidlem1  42215  lcfrlem9  42305  mapd1o  42403  mapdindp3  42477  zndvdchrrhm  42721  elre0re  43003  mullt0b2d  43239  flt0  43352  ismrc  43415  pellexlem1  43539  aomclem4  43767  dfac21  43776  lsmfgcl  43784  lmhmfgima  43794  dfacbasgrp  43818  hbtlem6  43839  fiuneneq  43902  oaabsb  44004  cantnfresb  44034  orbitcl  45649  stoweidlem27  46724  stoweidlem29  46726  fcoresf1  47789  tz6.12c-afv2  47962  dfatbrafv2b  47965  fnbrafv2b  47968  iccpartrn  48162  prmdvdsfmtnof1lem2  48320  mod42tp1mod8  48337  isubgredg  48614  grimuhgr  48635  grimcnv  48636  isuspgrim0  48642  assintopass  48962  rrxsphere  49511