Theorem syl5ibcom 244

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimpcd  248  elrab3t  3643  mob2  3672  rmob  3845  sneqrg  4796  preq1b  4803  prel12g  4820  disjxun  5102  sotric  5572  sotrieq  5573  iss  5988  poirr2  6077  xp11  6126  nordeq  6335  nsuceq0  6399  ordequn  6419  tz6.12cOLD  6867  fnbrfvb  6893  foeqcnvco  7243  f1eqcocnv  7244  f1eqcocnvOLD  7245  dfwe2  7705  releldmdifi  7974  mposn  8032  poxp2  8072  poxp3  8079  poseq  8087  tfrlem15  8335  tz7.44-2  8350  tz7.48-1  8386  tz7.49  8388  oawordexr  8500  oewordi  8535  oeeulem  8545  nna0r  8553  nnawordex  8581  nnaordex  8582  oaabs  8591  oaabs2  8592  eldifsucnn  8607  ectocld  8720  ecoptocl  8743  mapsnd  8821  eqeng  8923  difsnen  8994  fopwdom  9021  nneneq  9150  frfi  9229  elfiun  9363  ordiso  9449  ordtypelem7  9457  wemaplem2  9480  suc11reg  9552  inf3lem6  9566  noinfep  9593  cantnff  9607  cantnfp1lem2  9612  cantnfp1lem3  9613  cantnflem1  9622  cantnf  9626  ttrcltr  9649  r111  9708  rankc2  9804  tcrank  9817  cardnueq0  9897  fodomfi2  9993  alephinit  10028  dfac9  10069  dfac12k  10080  djuinf  10121  ackbij1  10171  ackbij2  10176  sornom  10210  fin23lem16  10268  fin23lem21  10272  isf32lem2  10287  fin1a2lem6  10338  itunitc  10354  zorn2lem4  10432  wunr1om  10652  tskr1om  10700  recmulnq  10897  ltexnq  10908  distrlem4pr  10959  1re  11152  0re  11154  0cnALT  11386  0cnALT2  11387  mulge0  11670  prodgt0  11999  peano2nn  12162  recnz  12575  zneo  12583  uzn0  12777  xlemul1a  13204  prunioo  13395  flidz  13712  ceilidz  13754  modid2  13800  modmuladdnn0  13817  om2uzrani  13854  uzrdgfni  13860  seqid  13950  seqz  13953  facdiv  14184  facwordi  14186  hashdom  14276  wrdnval  14430  wrdnfi  14433  wrdl1s1  14499  sqrmo  15133  fsumf1o  15605  isumltss  15730  supcvg  15738  dvdsnegb  16153  dvdsexp2im  16206  odd2np1lem  16219  odd2np1  16220  ltoddhalfle  16240  halfleoddlt  16241  opoe  16242  omoe  16243  opeo  16244  omeo  16245  bitsuz  16351  bezoutlem4  16420  gcddiv  16429  gcdzeq  16430  dvdssqim  16432  lcmgcdeq  16485  coprmdvds2  16527  rpmul  16532  divgcdcoprmex  16539  cncongr2  16541  dvdsprm  16576  coprm  16584  prmdvdsexp  16588  prmdiv  16654  pythagtriplem19  16702  pc2dvds  16748  pcadd  16758  prmpwdvds  16773  vdwlem11  16860  ramubcl  16887  0ram  16889  posasymb  18205  pleval2  18223  pltval3  18225  plttr  18228  pospo  18231  letsr  18479  intopsn  18506  ismgmid  18517  imasmnd2  18590  isgrpid2  18784  isgrpinv  18800  dfgrp3lem  18841  imasgrp2  18858  orbsta  19089  symgfix2  19194  pmtrfrn  19236  pmtrrn2  19238  odmulg  19334  odmulgeq  19335  gexdvdsi  19361  gexnnod  19366  pgpssslw  19392  sylow2alem1  19395  fislw  19403  lsmss1b  19444  lsmss2b  19446  efgrelexlemb  19528  torsubg  19628  ablfacrplem  19840  pgpfac1lem2  19850  pgpfac1lem3  19852  ablsimpnosubgd  19879  imasring  20041  dvdsrcl2  20075  dvdsrtr  20077  dvdsrmul1  20078  irredn0  20128  lspsneq0  20469  lmhmima  20504  lspsolv  20600  xrsdsreclblem  20839  dvdsrzring  20878  prmirredlem  20889  znunit  20966  pjdm2  21113  obselocv  21130  lindfrn  21223  opsrtoslem2  21459  mpfind  21513  mpfpf1  21713  pf1mpf  21714  cpmadugsumlemF  22221  baspartn  22300  bastop  22327  iscld3  22411  isopn3  22413  iscldtop  22442  ordtrest2lem  22550  2ndcredom  22797  2ndc1stc  22798  2ndcrest  22801  2ndcdisj  22803  2ndcsep  22806  kgenidm  22894  dfac14  22965  tx2ndc  22998  kqreglem1  23088  rnelfm  23300  fmfnfmlem2  23302  fmfnfmlem4  23304  fmfnfm  23305  flimtopon  23317  fclstopon  23359  xrsmopn  24171  icccmplem2  24182  reconnlem1  24185  iccpnfcnv  24303  cphsqrtcl2  24546  ivthlem3  24813  ivthicc  24818  ovolctb  24850  ioombl  24925  itgabs  25195  itgsplitioo  25198  dvlip  25353  c1liplem1  25356  c1lip1  25357  dvgt0lem1  25362  dvivthlem2  25369  dvne0  25371  lhop1lem  25373  lhop1  25374  lhop2  25375  lhop  25376  dvcvx  25380  itgsubstlem  25408  mdegnn0cl  25432  ig1peu  25532  elply2  25553  plypf1  25569  dgreq0  25622  aannenlem3  25686  abelthlem2  25787  lognegb  25941  eflogeq  25953  efopn  26009  cxpge0  26034  cxplea  26047  cxple2  26048  cxpcn3lem  26096  cxpaddlelem  26100  cxpaddle  26101  cxpeq  26106  asinsinb  26243  acoscosb  26244  atantanb  26270  wilthlem2  26414  sqf11  26484  sqff1o  26527  ppiublem1  26546  lgsdir  26676  lgsne0  26679  lgsquadlem3  26726  2sqblem  26775  dchrisum0flblem1  26852  ostth3  26982  ostth  26983  noseponlem  27008  nodenselem4  27031  nodenselem5  27032  nodenselem7  27034  nodenselem8  27035  nolt02o  27039  nogt01o  27040  nosupbnd2lem1  27059  noetasuplem4  27080  slerec  27154  madebdayim  27213  colinearalg  27757  axcontlem5  27815  axcontlem9  27819  uhgrn0  27916  upgrfn  27936  umgrfn  27948  uvtxnbgrvtx  28239  vtxduhgr0nedg  28338  pthdivtx  28575  iswwlksnx  28683  wpthswwlks2on  28804  clwwlkn  28868  clwwlknonwwlknonb  28948  eupth2lem2  29061  eupth2lem3lem6  29075  htthlem  29757  pjpreeq  30238  h1dn0  30392  spansneleqi  30409  rnbra  30947  dfpjop  31022  elpjrn  31030  stm1i  31083  mdbr2  31136  mdsl2i  31162  sumdmdlem  31258  dmdbr6ati  31263  ordtrest2NEWlem  32394  xrge0iifcnv  32405  eulerpartlemb  32859  erdszelem8  33683  cvmlift3lem4  33807  cvmlift3lem5  33808  fmlasucdisj  33884  mrsub0  34001  mrsubccat  34003  mrsubcn  34004  msubrn  34014  msrid  34030  elmthm  34061  dfon2lem9  34258  negsproplem2  34353  btwnconn1lem11  34671  broutsideof2  34696  opnbnd  34786  tailfb  34838  bj-ideqg1  35624  fin2so  36054  lindsadd  36060  poimirlem9  36076  poimirlem17  36084  poimirlem26  36093  poimirlem27  36094  poimirlem31  36098  itgabsnc  36136  ftc2nc  36149  sdclem2  36190  subspopn  36200  equivtotbnd  36226  rngosn3  36372  igenval2  36514  isfldidl  36516  relcnveq3  36771  ecex2  36778  iss2  36794  elrelscnveq3  36942  lshpinN  37440  lsatcv0eq  37498  lsatcv1  37499  cvrnbtwn3  37727  cvrnbtwn4  37730  cvrcmp  37734  atnlt  37764  cvlexchb1  37781  2llnne2N  37860  atcvr0eq  37878  lnnat  37879  cvrat4  37895  ps-1  37929  3at  37942  llncmp  37974  llnnlt  37975  llncvrlpln2  38009  llncvrlpln  38010  lplncmp  38014  lplnnlt  38017  lplncvrlvol2  38067  lplncvrlvol  38068  lvolcmp  38069  lvolnltN  38070  dalempnes  38103  dalemqnet  38104  dalem-cly  38123  dalem44  38168  lncmp  38235  cdlemblem  38245  llnexch2N  38322  osumcllem4N  38411  pexmidlem1N  38422  lhp2atnle  38485  cdleme11dN  38714  cdleme20k  38771  cdleme21at  38780  cdleme21ct  38781  cdleme32e  38897  cdleme35f  38906  tendoex  39427  dochexmidlem1  39912  lcfrlem9  40002  mapd1o  40100  mapdindp3  40174  elre0re  40753  dvdsexpim  40790  flt0  40951  ismrc  41000  pellexlem1  41128  aomclem4  41360  dfac21  41369  lsmfgcl  41377  lmhmfgima  41387  dfacbasgrp  41411  hbtlem6  41432  fiuneneq  41500  cantnfresb  41634  stoweidlem27  44238  stoweidlem29  44240  fcoresf1  45273  tz6.12c-afv2  45444  dfatbrafv2b  45447  fnbrafv2b  45450  iccpartrn  45592  prmdvdsfmtnof1lem2  45747  mod42tp1mod8  45764  assintopass  46118  rrxsphere  46804