Theorem syl5ibcom 247

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimpcd  251  elrab3t  3648  mob2  3676  rmob  3841  sneqrg  4794  preq1b  4801  prel12g  4819  disjxun  5095  sotric  5581  sotrieq  5582  iss  6019  poirr2  6106  xp11  6155  nordeq  6359  nsuceq0  6425  ordequn  6445  fnbrfvb  6911  2f1fvneq  7238  foeqcnvco  7278  f1eqcocnv  7279  dfwe2  7751  releldmdifi  8020  mposn  8075  poxp2  8116  poxp3  8123  poseq  8131  tfrlem15  8356  tz7.44-2  8371  tz7.48-1  8407  tz7.49  8409  oawordexr  8518  oewordi  8554  oeeulem  8564  nna0r  8572  nnawordex  8600  nnaordex  8601  nnaordex2  8602  oaabs  8611  oaabs2  8612  eldifsucnn  8627  elecex  8722  ectocld  8757  ecoptocl  8782  mapsnd  8861  eqeng  8960  difsnen  9024  fopwdom  9050  nneneq  9167  frfi  9222  elfiun  9369  ordiso  9457  ordtypelem7  9465  wemaplem2  9488  suc11reg  9567  inf3lem6  9581  noinfep  9608  cantnff  9622  cantnfp1lem2  9627  cantnfp1lem3  9628  cantnflem1  9637  cantnf  9641  ttrcltr  9664  r111  9726  rankc2  9822  tcrank  9835  cardnueq0  9915  fodomfi2  10009  alephinit  10044  dfac9  10086  dfac12k  10097  djuinf  10138  ackbij1  10186  ackbij2  10191  sornom  10227  fin23lem16  10285  fin23lem21  10289  isf32lem2  10304  fin1a2lem6  10355  itunitc  10371  zorn2lem4  10449  wunr1om  10670  tskr1om  10718  recmulnq  10915  ltexnq  10926  distrlem4pr  10977  1re  11174  0re  11176  0cnALT  11411  0cnALT2  11412  mulge0  11698  prodgt0  12031  peano2nn  12215  recnz  12641  zneo  12649  uzn0  12849  xlemul1a  13284  prunioo  13478  flidz  13813  ceilidz  13855  modid2  13901  modmuladdnn0  13921  om2uzrani  13958  uzrdgfni  13964  seqid  14053  seqz  14056  facdiv  14293  facwordi  14295  hashdom  14385  wrdnval  14551  wrdnfi  14554  wrdl1s1  14621  sqrmo  15268  fsumf1o  15740  isumltss  15868  supcvg  15876  dvdsnegb  16297  dvdsexp2im  16351  odd2np1lem  16364  odd2np1  16365  ltoddhalfle  16385  halfleoddlt  16386  opoe  16387  omoe  16388  opeo  16389  omeo  16390  bitsuz  16498  bezoutlem4  16566  gcddiv  16575  gcdzeq  16576  dvdssqim  16578  dvdsexpim  16579  lcmgcdeq  16636  coprmdvds2  16678  rpmul  16683  divgcdcoprmex  16690  cncongr2  16692  dvdsprm  16728  coprm  16736  prmdvdsexp  16740  prmdiv  16810  pythagtriplem19  16859  pc2dvds  16905  pcadd  16915  prmpwdvds  16930  vdwlem11  17017  ramubcl  17044  0ram  17046  posasymb  18341  pleval2  18357  pltval3  18359  plttr  18362  pospo  18365  letsr  18615  intopsn  18678  ismgmid  18689  imasmnd2  18798  isgrpid2  19008  isgrpinv  19025  dfgrp3lem  19070  imasgrp2  19087  orbsta  19343  symgfix2  19446  pmtrfrn  19488  pmtrrn2  19490  odmulg  19586  odmulgeq  19587  gexdvdsi  19613  gexnnod  19618  pgpssslw  19644  sylow2alem1  19647  fislw  19655  lsmss1b  19696  lsmss2b  19698  efgrelexlemb  19780  torsubg  19884  ablfacrplem  20097  pgpfac1lem2  20107  pgpfac1lem3  20109  ablsimpnosubgd  20136  imasrng  20213  imasring  20365  dvdsrcl2  20401  dvdsrtr  20403  dvdsrmul1  20404  irredn0  20458  lspsneq0  21066  lmhmima  21101  lspsolv  21200  xrsdsreclblem  21452  dvdsrzring  21500  prmirredlem  21511  znunit  21602  pjdm2  21750  obselocv  21767  lindfrn  21860  opsrtoslem2  22096  mpfind  22155  psdmul  22218  mpfpf1  22401  pf1mpf  22402  cpmadugsumlemF  22923  baspartn  23001  bastop  23028  iscld3  23111  isopn3  23113  iscldtop  23142  ordtrest2lem  23250  2ndcredom  23497  2ndc1stc  23498  2ndcrest  23501  2ndcdisj  23503  2ndcsep  23506  kgenidm  23594  dfac14  23665  tx2ndc  23698  kqreglem1  23788  rnelfm  24000  fmfnfmlem2  24002  fmfnfmlem4  24004  fmfnfm  24005  flimtopon  24017  fclstopon  24059  xrsmopn  24860  icccmplem2  24871  reconnlem1  24874  iccpnfcnv  24993  cphsqrtcl2  25235  ivthlem3  25502  ivthicc  25507  ovolctb  25539  ioombl  25614  itgabs  25884  itgsplitioo  25887  dvlip  26042  c1liplem1  26045  c1lip1  26046  dvgt0lem1  26051  dvivthlem2  26058  dvne0  26060  lhop1lem  26062  lhop1  26063  lhop2  26064  lhop  26065  dvcvx  26069  itgsubstlem  26097  mdegnn0cl  26118  ig1peu  26222  elply2  26243  plypf1  26259  dgreq0  26312  aannenlem3  26381  abelthlem2  26482  lognegb  26642  eflogeq  26654  efopn  26710  cxpge0  26735  cxplea  26748  cxple2  26749  cxpcn3lem  26799  cxpaddlelem  26803  cxpaddle  26804  cxpeq  26809  asinsinb  26949  acoscosb  26950  atantanb  26976  wilthlem2  27120  sqf11  27190  sqff1o  27233  ppiublem1  27253  lgsdir  27383  lgsne0  27386  lgsquadlem3  27433  2sqblem  27482  dchrisum0flblem1  27559  ostth3  27689  ostth  27690  noseponlem  27715  nodenselem4  27738  nodenselem5  27739  nodenselem7  27741  nodenselem8  27742  nolt02o  27746  nogt01o  27747  nosupbnd2lem1  27766  noetasuplem4  27787  lesrec  27879  madebdayim  27968  negsproplem2  28109  negsunif  28135  negleft  28138  negright  28139  lemuls1ad  28262  precsexlem6  28292  precsexlem7  28293  noseqp1  28371  om2noseqlt  28379  noseqrdgfn  28386  bdayn0sf1o  28450  dfnns2  28452  bdayfinbndlem1  28547  colinearalg  29067  axcontlem5  29125  axcontlem9  29129  uhgrn0  29224  upgrfn  29244  umgrfn  29256  uvtxnbgrvtx  29550  vtxduhgr0nedg  29649  pthdivtx  29883  iswwlksnx  29996  wpthswwlks2on  30120  clwwlkn  30184  clwwlknonwwlknonb  30264  eupth2lem2  30377  eupth2lem3lem6  30391  htthlem  31076  pjpreeq  31557  h1dn0  31711  spansneleqi  31728  rnbra  32266  dfpjop  32341  elpjrn  32349  stm1i  32402  mdbr2  32455  mdsl2i  32481  sumdmdlem  32577  dmdbr6ati  32582  ordtrest2NEWlem  34179  xrge0iifcnv  34190  eulerpartlemb  34625  onvf1odlem4  35409  erdszelem8  35508  cvmlift3lem4  35632  cvmlift3lem5  35633  fmlasucdisj  35709  mrsub0  35826  mrsubccat  35828  mrsubcn  35829  msubrn  35839  msrid  35855  elmthm  35886  dfon2lem9  36099  btwnconn1lem11  36407  broutsideof2  36432  opnbnd  36645  tailfb  36697  tr0elw  36804  tr0el  36805  bj-ideqg1  37616  fin2so  38066  lindsadd  38072  poimirlem9  38088  poimirlem17  38096  poimirlem26  38105  poimirlem27  38106  poimirlem31  38110  itgabsnc  38148  ftc2nc  38161  sdclem2  38201  subspopn  38211  equivtotbnd  38237  rngosn3  38383  igenval2  38525  isfldidl  38527  relcnveq3  38786  iss2  38803  elrelscnveq3  39086  lshpinN  39573  lsatcv0eq  39631  lsatcv1  39632  cvrnbtwn3  39860  cvrnbtwn4  39863  cvrcmp  39867  atnlt  39897  cvlexchb1  39914  2llnne2N  39992  atcvr0eq  40010  lnnat  40011  cvrat4  40027  ps-1  40061  3at  40074  llncmp  40106  llnnlt  40107  llncvrlpln2  40141  llncvrlpln  40142  lplncmp  40146  lplnnlt  40149  lplncvrlvol2  40199  lplncvrlvol  40200  lvolcmp  40201  lvolnltN  40202  dalempnes  40235  dalemqnet  40236  dalem-cly  40255  dalem44  40300  lncmp  40367  cdlemblem  40377  llnexch2N  40454  osumcllem4N  40543  pexmidlem1N  40554  lhp2atnle  40617  cdleme11dN  40846  cdleme20k  40903  cdleme21at  40912  cdleme21ct  40913  cdleme32e  41029  cdleme35f  41038  tendoex  41559  dochexmidlem1  42044  lcfrlem9  42134  mapd1o  42232  mapdindp3  42306  zndvdchrrhm  42550  elre0re  42830  mullt0b2d  43066  flt0  43179  ismrc  43242  pellexlem1  43366  aomclem4  43594  dfac21  43603  lsmfgcl  43611  lmhmfgima  43621  dfacbasgrp  43645  hbtlem6  43666  fiuneneq  43729  oaabsb  43831  cantnfresb  43861  orbitcl  45493  stoweidlem27  46561  stoweidlem29  46563  fcoresf1  47623  tz6.12c-afv2  47796  dfatbrafv2b  47799  fnbrafv2b  47802  iccpartrn  47996  prmdvdsfmtnof1lem2  48154  mod42tp1mod8  48171  isubgredg  48448  grimuhgr  48469  grimcnv  48470  isuspgrim0  48476  assintopass  48796  rrxsphere  49330