Theorem syl5ibcom 245

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 244	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpcd  249  elrab3t  3649  mob2  3677  rmob  3844  sneqrg  4793  preq1b  4800  prel12g  4818  disjxun  5093  sotric  5561  sotrieq  5562  iss  5990  poirr2  6077  xp11  6128  nordeq  6330  nsuceq0  6396  ordequn  6416  fnbrfvb  6877  2f1fvneq  7201  foeqcnvco  7241  f1eqcocnv  7242  dfwe2  7714  releldmdifi  7987  mposn  8043  poxp2  8083  poxp3  8090  poseq  8098  tfrlem15  8321  tz7.44-2  8336  tz7.48-1  8372  tz7.49  8374  oawordexr  8481  oewordi  8516  oeeulem  8526  nna0r  8534  nnawordex  8562  nnaordex  8563  nnaordex2  8564  oaabs  8573  oaabs2  8574  eldifsucnn  8589  elecex  8682  ectocld  8716  ecoptocl  8741  mapsnd  8820  eqeng  8918  difsnen  8983  fopwdom  9009  nneneq  9130  frfi  9190  elfiun  9339  ordiso  9427  ordtypelem7  9435  wemaplem2  9458  suc11reg  9534  inf3lem6  9548  noinfep  9575  cantnff  9589  cantnfp1lem2  9594  cantnfp1lem3  9595  cantnflem1  9604  cantnf  9608  ttrcltr  9631  r111  9690  rankc2  9786  tcrank  9799  cardnueq0  9879  fodomfi2  9973  alephinit  10008  dfac9  10050  dfac12k  10061  djuinf  10102  ackbij1  10150  ackbij2  10155  sornom  10190  fin23lem16  10248  fin23lem21  10252  isf32lem2  10267  fin1a2lem6  10318  itunitc  10334  zorn2lem4  10412  wunr1om  10632  tskr1om  10680  recmulnq  10877  ltexnq  10888  distrlem4pr  10939  1re  11134  0re  11136  0cnALT  11369  0cnALT2  11370  mulge0  11656  prodgt0  11989  peano2nn  12158  recnz  12569  zneo  12577  uzn0  12770  xlemul1a  13208  prunioo  13402  flidz  13732  ceilidz  13774  modid2  13820  modmuladdnn0  13840  om2uzrani  13877  uzrdgfni  13883  seqid  13972  seqz  13975  facdiv  14212  facwordi  14214  hashdom  14304  wrdnval  14470  wrdnfi  14473  wrdl1s1  14539  sqrmo  15176  fsumf1o  15648  isumltss  15773  supcvg  15781  dvdsnegb  16202  dvdsexp2im  16256  odd2np1lem  16269  odd2np1  16270  ltoddhalfle  16290  halfleoddlt  16291  opoe  16292  omoe  16293  opeo  16294  omeo  16295  bitsuz  16403  bezoutlem4  16471  gcddiv  16480  gcdzeq  16481  dvdssqim  16483  dvdsexpim  16484  lcmgcdeq  16541  coprmdvds2  16583  rpmul  16588  divgcdcoprmex  16595  cncongr2  16597  dvdsprm  16632  coprm  16640  prmdvdsexp  16644  prmdiv  16714  pythagtriplem19  16763  pc2dvds  16809  pcadd  16819  prmpwdvds  16834  vdwlem11  16921  ramubcl  16948  0ram  16950  posasymb  18243  pleval2  18259  pltval3  18261  plttr  18264  pospo  18267  letsr  18517  intopsn  18546  ismgmid  18557  imasmnd2  18666  isgrpid2  18873  isgrpinv  18890  dfgrp3lem  18935  imasgrp2  18952  orbsta  19210  symgfix2  19313  pmtrfrn  19355  pmtrrn2  19357  odmulg  19453  odmulgeq  19454  gexdvdsi  19480  gexnnod  19485  pgpssslw  19511  sylow2alem1  19514  fislw  19522  lsmss1b  19563  lsmss2b  19565  efgrelexlemb  19647  torsubg  19751  ablfacrplem  19964  pgpfac1lem2  19974  pgpfac1lem3  19976  ablsimpnosubgd  20003  imasrng  20080  imasring  20233  dvdsrcl2  20269  dvdsrtr  20271  dvdsrmul1  20272  irredn0  20326  lspsneq0  20933  lmhmima  20969  lspsolv  21068  xrsdsreclblem  21337  dvdsrzring  21386  prmirredlem  21397  znunit  21488  pjdm2  21636  obselocv  21653  lindfrn  21746  opsrtoslem2  21979  mpfind  22030  psdmul  22069  mpfpf1  22254  pf1mpf  22255  cpmadugsumlemF  22779  baspartn  22857  bastop  22884  iscld3  22967  isopn3  22969  iscldtop  22998  ordtrest2lem  23106  2ndcredom  23353  2ndc1stc  23354  2ndcrest  23357  2ndcdisj  23359  2ndcsep  23362  kgenidm  23450  dfac14  23521  tx2ndc  23554  kqreglem1  23644  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem4  23860  fmfnfm  23861  flimtopon  23873  fclstopon  23915  xrsmopn  24717  icccmplem2  24728  reconnlem1  24731  iccpnfcnv  24858  cphsqrtcl2  25102  ivthlem3  25370  ivthicc  25375  ovolctb  25407  ioombl  25482  itgabs  25752  itgsplitioo  25755  dvlip  25914  c1liplem1  25917  c1lip1  25918  dvgt0lem1  25923  dvivthlem2  25930  dvne0  25932  lhop1lem  25934  lhop1  25935  lhop2  25936  lhop  25937  dvcvx  25941  itgsubstlem  25971  mdegnn0cl  25992  ig1peu  26096  elply2  26117  plypf1  26133  dgreq0  26187  aannenlem3  26254  abelthlem2  26358  lognegb  26515  eflogeq  26527  efopn  26583  cxpge0  26608  cxplea  26621  cxple2  26622  cxpcn3lem  26673  cxpaddlelem  26677  cxpaddle  26678  cxpeq  26683  asinsinb  26823  acoscosb  26824  atantanb  26850  wilthlem2  26995  sqf11  27065  sqff1o  27108  ppiublem1  27129  lgsdir  27259  lgsne0  27262  lgsquadlem3  27309  2sqblem  27358  dchrisum0flblem1  27435  ostth3  27565  ostth  27566  noseponlem  27592  nodenselem4  27615  nodenselem5  27616  nodenselem7  27618  nodenselem8  27619  nolt02o  27623  nogt01o  27624  nosupbnd2lem1  27643  noetasuplem4  27664  slerec  27748  madebdayim  27820  negsproplem2  27958  negsunif  27984  slemul1ad  28108  precsexlem6  28137  precsexlem7  28138  noseqp1  28208  om2noseqlt  28216  noseqrdgfn  28223  bdayn0sf1o  28282  dfnns2  28284  colinearalg  28873  axcontlem5  28931  axcontlem9  28935  uhgrn0  29030  upgrfn  29050  umgrfn  29062  uvtxnbgrvtx  29356  vtxduhgr0nedg  29456  pthdivtx  29690  iswwlksnx  29803  wpthswwlks2on  29924  clwwlkn  29988  clwwlknonwwlknonb  30068  eupth2lem2  30181  eupth2lem3lem6  30195  htthlem  30879  pjpreeq  31360  h1dn0  31514  spansneleqi  31531  rnbra  32069  dfpjop  32144  elpjrn  32152  stm1i  32205  mdbr2  32258  mdsl2i  32284  sumdmdlem  32380  dmdbr6ati  32385  ordtrest2NEWlem  33891  xrge0iifcnv  33902  eulerpartlemb  34338  onvf1odlem4  35081  erdszelem8  35173  cvmlift3lem4  35297  cvmlift3lem5  35298  fmlasucdisj  35374  mrsub0  35491  mrsubccat  35493  mrsubcn  35494  msubrn  35504  msrid  35520  elmthm  35551  dfon2lem9  35767  btwnconn1lem11  36073  broutsideof2  36098  opnbnd  36301  tailfb  36353  bj-ideqg1  37140  fin2so  37589  lindsadd  37595  poimirlem9  37611  poimirlem17  37619  poimirlem26  37628  poimirlem27  37629  poimirlem31  37633  itgabsnc  37671  ftc2nc  37684  sdclem2  37724  subspopn  37734  equivtotbnd  37760  rngosn3  37906  igenval2  38048  isfldidl  38050  relcnveq3  38297  iss2  38314  elrelscnveq3  38470  lshpinN  38970  lsatcv0eq  39028  lsatcv1  39029  cvrnbtwn3  39257  cvrnbtwn4  39260  cvrcmp  39264  atnlt  39294  cvlexchb1  39311  2llnne2N  39390  atcvr0eq  39408  lnnat  39409  cvrat4  39425  ps-1  39459  3at  39472  llncmp  39504  llnnlt  39505  llncvrlpln2  39539  llncvrlpln  39540  lplncmp  39544  lplnnlt  39547  lplncvrlvol2  39597  lplncvrlvol  39598  lvolcmp  39599  lvolnltN  39600  dalempnes  39633  dalemqnet  39634  dalem-cly  39653  dalem44  39698  lncmp  39765  cdlemblem  39775  llnexch2N  39852  osumcllem4N  39941  pexmidlem1N  39952  lhp2atnle  40015  cdleme11dN  40244  cdleme20k  40301  cdleme21at  40310  cdleme21ct  40311  cdleme32e  40427  cdleme35f  40436  tendoex  40957  dochexmidlem1  41442  lcfrlem9  41532  mapd1o  41630  mapdindp3  41704  zndvdchrrhm  41948  elre0re  42230  mullt0b2d  42460  flt0  42613  ismrc  42677  pellexlem1  42805  aomclem4  43033  dfac21  43042  lsmfgcl  43050  lmhmfgima  43060  dfacbasgrp  43084  hbtlem6  43105  fiuneneq  43168  oaabsb  43270  cantnfresb  43300  orbitcl  44934  stoweidlem27  46012  stoweidlem29  46014  fcoresf1  47057  tz6.12c-afv2  47230  dfatbrafv2b  47233  fnbrafv2b  47236  iccpartrn  47418  prmdvdsfmtnof1lem2  47573  mod42tp1mod8  47590  isubgredg  47854  grimuhgr  47875  grimcnv  47876  isuspgrim0  47882  assintopass  48202  rrxsphere  48737