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  3647  mob2  3676  rmob  3841  sneqrg  4799  preq1b  4806  prel12g  4824  disjxun  5106  sotric  5596  sotrieq  5597  iss  6045  poirr2  6136  xp11  6185  nordeq  6407  nsuceq0  6474  ordequn  6494  fnbrfvb  6966  2f1fvneq  7295  foeqcnvco  7339  f1eqcocnv  7340  dfwe2  7820  releldmdifi  8091  mposn  8151  poxp2  8197  poxp3  8204  poseq  8212  tfrlem15  8438  tz7.44-2  8453  tz7.48-1  8491  tz7.49  8493  oawordexr  8602  oewordi  8638  oeeulem  8648  nna0r  8656  nnawordex  8684  nnaordex  8685  nnaordex2  8686  oaabs  8695  oaabs2  8696  eldifsucnn  8711  elecex  8806  ectocld  8841  ecoptocl  8866  mapsnd  8952  eqeng  9051  difsnen  9116  fopwdom  9142  nneneq  9259  frfi  9314  elfiun  9459  ordiso  9547  ordtypelem7  9555  wemaplem2  9578  suc11reg  9657  inf3lem6  9671  noinfep  9698  cantnff  9712  cantnfp1lem2  9717  cantnfp1lem3  9718  cantnflem1  9727  cantnf  9731  ttrcltr  9754  r111  9819  rankc2  9925  tcrank  9938  cardnueq0  10082  fodomfi2  10178  alephinit  10213  dfac9  10254  dfac12k  10265  djuinf  10306  ackbij1  10354  ackbij2  10359  sornom  10394  fin23lem16  10452  fin23lem21  10456  isf32lem2  10471  fin1a2lem6  10522  itunitc  10538  zorn2lem4  10616  wunr1om  10843  tskr1om  10891  recmulnq  11088  ltexnq  11099  distrlem4pr  11150  1re  11347  0re  11349  0cnALT  11584  0cnALT2  11585  mulge0  11874  prodgt0  12204  peano2nn  12387  recnz  12814  zneo  12822  uzn0  13022  xlemul1a  13458  prunioo  13652  flidz  13990  ceilidz  14032  modid2  14078  modmuladdnn0  14098  om2uzrani  14135  uzrdgfni  14141  seqid  14230  seqz  14233  facdiv  14472  facwordi  14474  hashdom  14564  wrdnval  14731  wrdnfi  14734  wrdl1s1  14804  sqrmo  15461  fsumf1o  15933  isumltss  16061  supcvg  16069  dvdsnegb  16487  dvdsexp2im  16541  odd2np1lem  16554  odd2np1  16555  ltoddhalfle  16575  halfleoddlt  16576  opoe  16577  omoe  16578  opeo  16579  omeo  16580  bitsuz  16688  bezoutlem4  16759  gcddiv  16768  gcdzeq  16769  dvdssqim  16771  dvdsexpim  16772  lcmgcdeq  16831  coprmdvds2  16873  rpmul  16878  divgcdcoprmex  16885  cncongr2  16887  dvdsprm  16923  coprm  16931  prmdvdsexp  16935  prmdiv  17006  pythagtriplem19  17055  pc2dvds  17101  pcadd  17111  prmpwdvds  17126  vdwlem11  17213  ramubcl  17240  0ram  17242  posasymb  18543  pleval2  18559  pltval3  18561  plttr  18564  pospo  18567  letsr  18817  intopsn  18882  ismgmid  18895  imasmgm2  18913  imasmnd2  19018  isgrpid2  19237  isgrpinv  19254  dfgrp3lem  19298  imasgrp2  19315  orbsta  19578  symgfix2  19681  pmtrfrn  19723  pmtrrn2  19725  odmulg  19821  odmulgeq  19822  gexdvdsi  19848  gexnnod  19853  pgpssslw  19879  sylow2alem1  19882  fislw  19890  lsmss1b  19931  lsmss2b  19933  efgrelexlemb  20015  torsubg  20119  ablfacrplem  20332  pgpfac1lem2  20342  pgpfac1lem3  20344  ablsimpnosubgd  20371  imasrng  20450  imasring  20611  dvdsrcl2  20647  dvdsrtr  20649  dvdsrmul1  20650  irredn0  20704  lspsneq0  21338  lmhmima  21373  lspsolv  21472  rspprop  21575  xrsdsreclblem  21771  dvdsrzring  21822  prmirredlem  21833  znunit  21924  pjdm2  22072  obselocv  22089  lindfrn  22182  opsrtoslem2  22420  mpfind  22479  psdmul  22542  mpfpf1  22724  pf1mpf  22725  cpmadugsumlemF  23249  baspartn  23327  bastop  23354  iscld3  23437  isopn3  23439  iscldtop  23468  ordtrest2lem  23576  2ndcredom  23823  2ndc1stc  23824  2ndcrest  23827  2ndcdisj  23830  2ndcsep  23833  kgenidm  23921  dfac14  23992  tx2ndc  24025  kqreglem1  24115  rnelfm  24327  fmfnfmlem2  24329  fmfnfmlem4  24331  fmfnfm  24332  flimtopon  24344  fclstopon  24386  xrsmopn  25187  icccmplem2  25198  reconnlem1  25201  iccpnfcnv  25320  cphsqrtcl2  25562  ivthlem3  25829  ivthicc  25834  ovolctb  25866  ioombl  25941  itgabs  26210  itgsplitioo  26213  dvlip  26368  c1liplem1  26371  c1lip1  26372  dvgt0lem1  26377  dvivthlem2  26384  dvne0  26386  lhop1lem  26388  lhop1  26389  lhop2  26390  lhop  26391  dvcvx  26395  itgsubstlem  26423  mdegnn0cl  26444  ig1peu  26548  elply2  26569  plypf1  26586  dgreq0  26639  aannenlem3  26714  abelthlem2  26816  lognegb  26975  eflogeq  26987  efopn  27043  cxpge0  27068  cxplea  27081  cxple2  27082  cxpcn3lem  27132  cxpaddlelem  27136  cxpaddle  27137  cxpeq  27142  asinsinb  27282  acoscosb  27283  atantanb  27309  wilthlem2  27453  sqf11  27523  sqff1o  27566  ppiublem1  27586  lgsdir  27716  lgsne0  27719  lgsquadlem3  27766  2sqblem  27815  dchrisum0flblem1  27892  ostth3  28022  ostth  28023  flt0  28026  fltoprm  28052  noseponlem  28078  nodenselem4  28101  nodenselem5  28102  nodenselem7  28104  nodenselem8  28105  nolt02o  28109  nogt01o  28110  nosupbnd2lem1  28129  noetasuplem4  28150  lesrec  28242  madebdayim  28331  negsproplem2  28472  negsunif  28498  negleft  28501  negright  28502  lemuls1ad  28625  precsexlem6  28655  precsexlem7  28656  noseqp1  28734  om2noseqlt  28742  noseqrdgfn  28749  bdayn0sf1o  28813  dfnns2  28815  bdayfinbndlem1  28910  colinearalg  29545  axcontlem5  29603  axcontlem9  29607  uhgrn0  29702  upgrfn  29722  umgrfn  29734  uvtxnbgrvtx  30031  vtxduhgr0nedg  30130  pthdivtx  30369  iswwlksnx  30486  wpthswwlks2on  30610  clwwlkn  30674  clwwlknonwwlknonb  30754  eupth2lem2  30877  eupth2lem3lem6  30891  htthlem  31576  pjpreeq  32057  h1dn0  32211  spansneleqi  32228  rnbra  32766  dfpjop  32841  elpjrn  32849  stm1i  32902  mdbr2  32955  mdsl2i  32981  sumdmdlem  33077  dmdbr6ati  33082  ordtrest2NEWlem  34665  xrge0iifcnv  34676  eulerpartlemb  35111  maxssj0  36047  onvf1odlem4  36075  erdszelem8  36171  cvmlift3lem4  36295  cvmlift3lem5  36296  fmlasucdisj  36372  mrsub0  36489  mrsubccat  36491  mrsubcn  36492  msubrn  36502  msrid  36518  elmthm  36549  dfon2lem9  36768  btwnconn1lem11  37077  broutsideof2  37102  opnbnd  37328  tailfb  37380  tr0elw  37487  tr0el  37488  bj-ideqg1  38353  fin2so  38798  lindsadd  38804  poimirlem9  38815  poimirlem17  38823  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  itgabsnc  38875  ftc2nc  38888  sdclem2  38942  subspopn  38952  equivtotbnd  38978  rngosn3  39124  igenval2  39266  isfldidl  39268  relcnveq3  39525  iss2  39542  elrelscnveq3  39825  lshpinN  40312  lsatcv0eq  40370  lsatcv1  40371  cvrnbtwn3  40599  cvrnbtwn4  40602  cvrcmp  40606  atnlt  40636  cvlexchb1  40653  2llnne2N  40731  atcvr0eq  40749  lnnat  40750  cvrat4  40766  ps-1  40800  3at  40813  llncmp  40845  llnnlt  40846  llncvrlpln2  40880  llncvrlpln  40881  lplncmp  40885  lplnnlt  40888  lplncvrlvol2  40938  lplncvrlvol  40939  lvolcmp  40940  lvolnltN  40941  dalempnes  40974  dalemqnet  40975  dalem-cly  40994  dalem44  41039  lncmp  41106  cdlemblem  41116  llnexch2N  41193  osumcllem4N  41282  pexmidlem1N  41293  lhp2atnle  41356  cdleme11dN  41585  cdleme20k  41642  cdleme21at  41651  cdleme21ct  41652  cdleme32e  41768  cdleme35f  41777  tendoex  42298  dochexmidlem1  42783  lcfrlem9  42873  mapd1o  42971  mapdindp3  43045  zndvdchrrhm  43289  elre0re  43571  mullt0b2d  43814  ismrc  43978  pellexlem1  44102  aomclem4  44325  dfac21  44334  lsmfgcl  44342  lmhmfgima  44352  dfacbasgrp  44375  hbtlem6  44396  fiuneneq  44455  oaabsb  44557  cantnfresb  44587  orbitcl  46211  stoweidlem27  47310  stoweidlem29  47312  fcoresf1  48412  tz6.12c-afv2  48585  dfatbrafv2b  48588  fnbrafv2b  48591  iccpartrn  48785  prmdvdsfmtnof1lem2  48943  mod42tp1mod8  48960  isubgredg  49237  grimuhgr  49258  grimcnv  49259  isuspgrim0  49265  assintopass  49584  rrxsphere  50191