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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimpcd  252  elrab3t  3658  mob2  3687  rmob  3852  sneqrg  4805  preq1b  4812  prel12g  4830  disjxun  5108  sotric  5597  sotrieq  5598  iss  6035  poirr2  6122  xp11  6172  nordeq  6376  nsuceq0  6443  ordequn  6463  fnbrfvb  6929  2f1fvneq  7256  foeqcnvco  7296  f1eqcocnv  7297  dfwe2  7769  releldmdifi  8038  mposn  8094  poxp2  8135  poxp3  8142  poseq  8150  tfrlem15  8375  tz7.44-2  8390  tz7.48-1  8426  tz7.49  8428  oawordexr  8537  oewordi  8573  oeeulem  8583  nna0r  8591  nnawordex  8619  nnaordex  8620  nnaordex2  8621  oaabs  8630  oaabs2  8631  eldifsucnn  8646  elecex  8741  ectocld  8776  ecoptocl  8801  mapsnd  8880  eqeng  8979  difsnen  9043  fopwdom  9069  nneneq  9186  frfi  9241  elfiun  9386  ordiso  9474  ordtypelem7  9482  wemaplem2  9505  suc11reg  9584  inf3lem6  9598  noinfep  9625  cantnff  9639  cantnfp1lem2  9644  cantnfp1lem3  9645  cantnflem1  9654  cantnf  9658  ttrcltr  9681  r111  9743  rankc2  9839  tcrank  9852  cardnueq0  9946  fodomfi2  10040  alephinit  10075  dfac9  10116  dfac12k  10127  djuinf  10168  ackbij1  10216  ackbij2  10221  sornom  10257  fin23lem16  10315  fin23lem21  10319  isf32lem2  10334  fin1a2lem6  10385  itunitc  10401  zorn2lem4  10479  wunr1om  10700  tskr1om  10748  recmulnq  10945  ltexnq  10956  distrlem4pr  11007  1re  11204  0re  11206  0cnALT  11441  0cnALT2  11442  mulge0  11728  prodgt0  12058  peano2nn  12241  recnz  12667  zneo  12675  uzn0  12875  xlemul1a  13310  prunioo  13504  flidz  13839  ceilidz  13881  modid2  13927  modmuladdnn0  13947  om2uzrani  13984  uzrdgfni  13990  seqid  14079  seqz  14082  facdiv  14319  facwordi  14321  hashdom  14411  wrdnval  14578  wrdnfi  14581  wrdl1s1  14648  sqrmo  15298  fsumf1o  15770  isumltss  15898  supcvg  15906  dvdsnegb  16327  dvdsexp2im  16381  odd2np1lem  16394  odd2np1  16395  ltoddhalfle  16415  halfleoddlt  16416  opoe  16417  omoe  16418  opeo  16419  omeo  16420  bitsuz  16528  bezoutlem4  16596  gcddiv  16605  gcdzeq  16606  dvdssqim  16608  dvdsexpim  16609  lcmgcdeq  16666  coprmdvds2  16708  rpmul  16713  divgcdcoprmex  16720  cncongr2  16722  dvdsprm  16758  coprm  16766  prmdvdsexp  16770  prmdiv  16840  pythagtriplem19  16889  pc2dvds  16935  pcadd  16945  prmpwdvds  16960  vdwlem11  17047  ramubcl  17074  0ram  17076  posasymb  18371  pleval2  18387  pltval3  18389  plttr  18392  pospo  18395  letsr  18645  intopsn  18708  ismgmid  18719  imasmnd2  18828  isgrpid2  19039  isgrpinv  19056  dfgrp3lem  19100  imasgrp2  19117  orbsta  19379  symgfix2  19482  pmtrfrn  19524  pmtrrn2  19526  odmulg  19622  odmulgeq  19623  gexdvdsi  19649  gexnnod  19654  pgpssslw  19680  sylow2alem1  19683  fislw  19691  lsmss1b  19732  lsmss2b  19734  efgrelexlemb  19816  torsubg  19920  ablfacrplem  20133  pgpfac1lem2  20143  pgpfac1lem3  20145  ablsimpnosubgd  20172  imasrng  20251  imasring  20408  dvdsrcl2  20444  dvdsrtr  20446  dvdsrmul1  20447  irredn0  20501  lspsneq0  21107  lmhmima  21142  lspsolv  21241  xrsdsreclblem  21528  dvdsrzring  21576  prmirredlem  21587  znunit  21678  pjdm2  21826  obselocv  21843  lindfrn  21936  opsrtoslem2  22172  mpfind  22231  psdmul  22294  mpfpf1  22476  pf1mpf  22477  cpmadugsumlemF  22998  baspartn  23076  bastop  23103  iscld3  23186  isopn3  23188  iscldtop  23217  ordtrest2lem  23325  2ndcredom  23572  2ndc1stc  23573  2ndcrest  23576  2ndcdisj  23578  2ndcsep  23581  kgenidm  23669  dfac14  23740  tx2ndc  23773  kqreglem1  23863  rnelfm  24075  fmfnfmlem2  24077  fmfnfmlem4  24079  fmfnfm  24080  flimtopon  24092  fclstopon  24134  xrsmopn  24935  icccmplem2  24946  reconnlem1  24949  iccpnfcnv  25068  cphsqrtcl2  25310  ivthlem3  25577  ivthicc  25582  ovolctb  25614  ioombl  25689  itgabs  25959  itgsplitioo  25962  dvlip  26117  c1liplem1  26120  c1lip1  26121  dvgt0lem1  26126  dvivthlem2  26133  dvne0  26135  lhop1lem  26137  lhop1  26138  lhop2  26139  lhop  26140  dvcvx  26144  itgsubstlem  26172  mdegnn0cl  26193  ig1peu  26297  elply2  26318  plypf1  26334  dgreq0  26387  aannenlem3  26456  abelthlem2  26557  lognegb  26717  eflogeq  26729  efopn  26785  cxpge0  26810  cxplea  26823  cxple2  26824  cxpcn3lem  26874  cxpaddlelem  26878  cxpaddle  26879  cxpeq  26884  asinsinb  27024  acoscosb  27025  atantanb  27051  wilthlem2  27195  sqf11  27265  sqff1o  27308  ppiublem1  27328  lgsdir  27458  lgsne0  27461  lgsquadlem3  27508  2sqblem  27557  dchrisum0flblem1  27634  ostth3  27764  ostth  27765  noseponlem  27790  nodenselem4  27813  nodenselem5  27814  nodenselem7  27816  nodenselem8  27817  nolt02o  27821  nogt01o  27822  nosupbnd2lem1  27841  noetasuplem4  27862  lesrec  27954  madebdayim  28043  negsproplem2  28184  negsunif  28210  negleft  28213  negright  28214  lemuls1ad  28337  precsexlem6  28367  precsexlem7  28368  noseqp1  28446  om2noseqlt  28454  noseqrdgfn  28461  bdayn0sf1o  28525  dfnns2  28527  bdayfinbndlem1  28622  colinearalg  29197  axcontlem5  29255  axcontlem9  29259  uhgrn0  29354  upgrfn  29374  umgrfn  29386  uvtxnbgrvtx  29680  vtxduhgr0nedg  29779  pthdivtx  30013  iswwlksnx  30126  wpthswwlks2on  30250  clwwlkn  30314  clwwlknonwwlknonb  30394  eupth2lem2  30507  eupth2lem3lem6  30521  htthlem  31206  pjpreeq  31687  h1dn0  31841  spansneleqi  31858  rnbra  32396  dfpjop  32471  elpjrn  32479  stm1i  32532  mdbr2  32585  mdsl2i  32611  sumdmdlem  32707  dmdbr6ati  32712  ordtrest2NEWlem  34253  xrge0iifcnv  34264  eulerpartlemb  34699  onvf1odlem4  35485  erdszelem8  35585  cvmlift3lem4  35709  cvmlift3lem5  35710  fmlasucdisj  35786  mrsub0  35903  mrsubccat  35905  mrsubcn  35906  msubrn  35916  msrid  35932  elmthm  35963  dfon2lem9  36176  btwnconn1lem11  36484  broutsideof2  36509  opnbnd  36721  tailfb  36773  tr0elw  36880  tr0el  36881  bj-ideqg1  37691  fin2so  38141  lindsadd  38147  poimirlem9  38163  poimirlem17  38171  poimirlem26  38180  poimirlem27  38181  poimirlem31  38185  itgabsnc  38223  ftc2nc  38236  sdclem2  38276  subspopn  38286  equivtotbnd  38312  rngosn3  38458  igenval2  38600  isfldidl  38602  relcnveq3  38861  iss2  38878  elrelscnveq3  39161  lshpinN  39648  lsatcv0eq  39706  lsatcv1  39707  cvrnbtwn3  39935  cvrnbtwn4  39938  cvrcmp  39942  atnlt  39972  cvlexchb1  39989  2llnne2N  40067  atcvr0eq  40085  lnnat  40086  cvrat4  40102  ps-1  40136  3at  40149  llncmp  40181  llnnlt  40182  llncvrlpln2  40216  llncvrlpln  40217  lplncmp  40221  lplnnlt  40224  lplncvrlvol2  40274  lplncvrlvol  40275  lvolcmp  40276  lvolnltN  40277  dalempnes  40310  dalemqnet  40311  dalem-cly  40330  dalem44  40375  lncmp  40442  cdlemblem  40452  llnexch2N  40529  osumcllem4N  40618  pexmidlem1N  40629  lhp2atnle  40692  cdleme11dN  40921  cdleme20k  40978  cdleme21at  40987  cdleme21ct  40988  cdleme32e  41104  cdleme35f  41113  tendoex  41634  dochexmidlem1  42119  lcfrlem9  42209  mapd1o  42307  mapdindp3  42381  zndvdchrrhm  42625  elre0re  42905  mullt0b2d  43141  flt0  43254  ismrc  43317  pellexlem1  43441  aomclem4  43669  dfac21  43678  lsmfgcl  43686  lmhmfgima  43696  dfacbasgrp  43720  hbtlem6  43741  fiuneneq  43804  oaabsb  43906  cantnfresb  43936  orbitcl  45551  stoweidlem27  46626  stoweidlem29  46628  fcoresf1  47688  tz6.12c-afv2  47861  dfatbrafv2b  47864  fnbrafv2b  47867  iccpartrn  48061  prmdvdsfmtnof1lem2  48219  mod42tp1mod8  48236  isubgredg  48513  grimuhgr  48534  grimcnv  48535  isuspgrim0  48541  assintopass  48861  rrxsphere  49406