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 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimpcd  252  elrab3t  3651  mob2  3680  rmob  3844  sneqrg  4806  preq1b  4813  prel12g  4831  disjxun  5109  sotric  5601  sotrieq  5602  iss  6039  poirr2  6126  xp11  6175  nordeq  6383  nsuceq0  6450  ordequn  6470  fnbrfvb  6935  2f1fvneq  7260  foeqcnvco  7304  f1eqcocnv  7305  dfwe2  7775  releldmdifi  8044  mposn  8100  poxp2  8141  poxp3  8148  poseq  8156  tfrlem15  8381  tz7.44-2  8396  tz7.48-1  8432  tz7.49  8434  oawordexr  8543  oewordi  8579  oeeulem  8589  nna0r  8597  nnawordex  8625  nnaordex  8626  nnaordex2  8627  oaabs  8636  oaabs2  8637  eldifsucnn  8652  elecex  8747  ectocld  8782  ecoptocl  8807  mapsnd  8886  eqeng  8985  difsnen  9050  fopwdom  9076  nneneq  9193  frfi  9248  elfiun  9393  ordiso  9481  ordtypelem7  9489  wemaplem2  9512  suc11reg  9591  inf3lem6  9605  noinfep  9632  cantnff  9646  cantnfp1lem2  9651  cantnfp1lem3  9652  cantnflem1  9661  cantnf  9665  ttrcltr  9688  r111  9750  rankc2  9846  tcrank  9859  cardnueq0  9962  fodomfi2  10056  alephinit  10091  dfac9  10132  dfac12k  10143  djuinf  10184  ackbij1  10232  ackbij2  10237  sornom  10272  fin23lem16  10330  fin23lem21  10334  isf32lem2  10349  fin1a2lem6  10400  itunitc  10416  zorn2lem4  10494  wunr1om  10715  tskr1om  10763  recmulnq  10960  ltexnq  10971  distrlem4pr  11022  1re  11219  0re  11221  0cnALT  11456  0cnALT2  11457  mulge0  11743  prodgt0  12073  peano2nn  12256  recnz  12682  zneo  12690  uzn0  12890  xlemul1a  13325  prunioo  13519  flidz  13856  ceilidz  13898  modid2  13944  modmuladdnn0  13964  om2uzrani  14001  uzrdgfni  14007  seqid  14096  seqz  14099  facdiv  14336  facwordi  14338  hashdom  14428  wrdnval  14595  wrdnfi  14598  wrdl1s1  14667  sqrmo  15321  fsumf1o  15792  isumltss  15920  supcvg  15928  dvdsnegb  16348  dvdsexp2im  16402  odd2np1lem  16415  odd2np1  16416  ltoddhalfle  16436  halfleoddlt  16437  opoe  16438  omoe  16439  opeo  16440  omeo  16441  bitsuz  16549  bezoutlem4  16617  gcddiv  16626  gcdzeq  16627  dvdssqim  16629  dvdsexpim  16630  lcmgcdeq  16687  coprmdvds2  16729  rpmul  16734  divgcdcoprmex  16741  cncongr2  16743  dvdsprm  16779  coprm  16787  prmdvdsexp  16791  prmdiv  16861  pythagtriplem19  16910  pc2dvds  16956  pcadd  16966  prmpwdvds  16981  vdwlem11  17068  ramubcl  17095  0ram  17097  posasymb  18392  pleval2  18408  pltval3  18410  plttr  18413  pospo  18416  letsr  18666  intopsn  18729  ismgmid  18740  imasmnd2  18855  isgrpid2  19066  isgrpinv  19083  dfgrp3lem  19127  imasgrp2  19144  orbsta  19406  symgfix2  19509  pmtrfrn  19551  pmtrrn2  19553  odmulg  19649  odmulgeq  19650  gexdvdsi  19676  gexnnod  19681  pgpssslw  19707  sylow2alem1  19710  fislw  19718  lsmss1b  19759  lsmss2b  19761  efgrelexlemb  19843  torsubg  19947  ablfacrplem  20160  pgpfac1lem2  20170  pgpfac1lem3  20172  ablsimpnosubgd  20199  imasrng  20278  imasring  20437  dvdsrcl2  20473  dvdsrtr  20475  dvdsrmul1  20476  irredn0  20530  lspsneq0  21162  lmhmima  21197  lspsolv  21296  rspprop  21399  xrsdsreclblem  21592  dvdsrzring  21640  prmirredlem  21651  znunit  21742  pjdm2  21890  obselocv  21907  lindfrn  22000  opsrtoslem2  22236  mpfind  22295  psdmul  22358  mpfpf1  22540  pf1mpf  22541  cpmadugsumlemF  23062  baspartn  23140  bastop  23167  iscld3  23250  isopn3  23252  iscldtop  23281  ordtrest2lem  23389  2ndcredom  23636  2ndc1stc  23637  2ndcrest  23640  2ndcdisj  23642  2ndcsep  23645  kgenidm  23733  dfac14  23804  tx2ndc  23837  kqreglem1  23927  rnelfm  24139  fmfnfmlem2  24141  fmfnfmlem4  24143  fmfnfm  24144  flimtopon  24156  fclstopon  24198  xrsmopn  24999  icccmplem2  25010  reconnlem1  25013  iccpnfcnv  25132  cphsqrtcl2  25374  ivthlem3  25641  ivthicc  25646  ovolctb  25678  ioombl  25753  itgabs  26023  itgsplitioo  26026  dvlip  26181  c1liplem1  26184  c1lip1  26185  dvgt0lem1  26190  dvivthlem2  26197  dvne0  26199  lhop1lem  26201  lhop1  26202  lhop2  26203  lhop  26204  dvcvx  26208  itgsubstlem  26236  mdegnn0cl  26257  ig1peu  26361  elply2  26382  plypf1  26398  dgreq0  26451  aannenlem3  26522  abelthlem2  26624  lognegb  26784  eflogeq  26796  efopn  26852  cxpge0  26877  cxplea  26890  cxple2  26891  cxpcn3lem  26941  cxpaddlelem  26945  cxpaddle  26946  cxpeq  26951  asinsinb  27091  acoscosb  27092  atantanb  27118  wilthlem2  27262  sqf11  27332  sqff1o  27375  ppiublem1  27395  lgsdir  27525  lgsne0  27528  lgsquadlem3  27575  2sqblem  27624  dchrisum0flblem1  27701  ostth3  27831  ostth  27832  noseponlem  27857  nodenselem4  27880  nodenselem5  27881  nodenselem7  27883  nodenselem8  27884  nolt02o  27888  nogt01o  27889  nosupbnd2lem1  27908  noetasuplem4  27929  lesrec  28021  madebdayim  28110  negsproplem2  28251  negsunif  28277  negleft  28280  negright  28281  lemuls1ad  28404  precsexlem6  28434  precsexlem7  28435  noseqp1  28513  om2noseqlt  28521  noseqrdgfn  28528  bdayn0sf1o  28592  dfnns2  28594  bdayfinbndlem1  28689  colinearalg  29289  axcontlem5  29347  axcontlem9  29351  uhgrn0  29446  upgrfn  29466  umgrfn  29478  uvtxnbgrvtx  29772  vtxduhgr0nedg  29871  pthdivtx  30105  iswwlksnx  30218  wpthswwlks2on  30342  clwwlkn  30406  clwwlknonwwlknonb  30486  eupth2lem2  30599  eupth2lem3lem6  30613  htthlem  31298  pjpreeq  31779  h1dn0  31933  spansneleqi  31950  rnbra  32488  dfpjop  32563  elpjrn  32571  stm1i  32624  mdbr2  32677  mdsl2i  32703  sumdmdlem  32799  dmdbr6ati  32804  ordtrest2NEWlem  34335  xrge0iifcnv  34346  eulerpartlemb  34782  onvf1odlem4  35606  erdszelem8  35703  cvmlift3lem4  35827  cvmlift3lem5  35828  fmlasucdisj  35904  mrsub0  36021  mrsubccat  36023  mrsubcn  36024  msubrn  36034  msrid  36050  elmthm  36081  dfon2lem9  36294  btwnconn1lem11  36602  broutsideof2  36627  opnbnd  36869  tailfb  36921  tr0elw  37028  tr0el  37029  bj-ideqg1  37841  fin2so  38291  lindsadd  38297  poimirlem9  38313  poimirlem17  38321  poimirlem26  38330  poimirlem27  38331  poimirlem31  38335  itgabsnc  38373  ftc2nc  38386  sdclem2  38426  subspopn  38436  equivtotbnd  38462  rngosn3  38608  igenval2  38750  isfldidl  38752  relcnveq3  39009  iss2  39026  elrelscnveq3  39309  lshpinN  39796  lsatcv0eq  39854  lsatcv1  39855  cvrnbtwn3  40083  cvrnbtwn4  40086  cvrcmp  40090  atnlt  40120  cvlexchb1  40137  2llnne2N  40215  atcvr0eq  40233  lnnat  40234  cvrat4  40250  ps-1  40284  3at  40297  llncmp  40329  llnnlt  40330  llncvrlpln2  40364  llncvrlpln  40365  lplncmp  40369  lplnnlt  40372  lplncvrlvol2  40422  lplncvrlvol  40423  lvolcmp  40424  lvolnltN  40425  dalempnes  40458  dalemqnet  40459  dalem-cly  40478  dalem44  40523  lncmp  40590  cdlemblem  40600  llnexch2N  40677  osumcllem4N  40766  pexmidlem1N  40777  lhp2atnle  40840  cdleme11dN  41069  cdleme20k  41126  cdleme21at  41135  cdleme21ct  41136  cdleme32e  41252  cdleme35f  41261  tendoex  41782  dochexmidlem1  42267  lcfrlem9  42357  mapd1o  42455  mapdindp3  42529  zndvdchrrhm  42773  elre0re  43055  mullt0b2d  43291  flt0  43402  ismrc  43465  pellexlem1  43589  aomclem4  43817  dfac21  43826  lsmfgcl  43834  lmhmfgima  43844  dfacbasgrp  43868  hbtlem6  43889  fiuneneq  43952  oaabsb  44054  cantnfresb  44084  orbitcl  45699  stoweidlem27  46774  stoweidlem29  46776  fcoresf1  47839  tz6.12c-afv2  48012  dfatbrafv2b  48015  fnbrafv2b  48018  iccpartrn  48212  prmdvdsfmtnof1lem2  48370  mod42tp1mod8  48387  isubgredg  48664  grimuhgr  48685  grimcnv  48686  isuspgrim0  48692  assintopass  49012  rrxsphere  49561