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  3644  mob2  3673  rmob  3837  sneqrg  4799  preq1b  4806  prel12g  4824  disjxun  5101  sotric  5589  sotrieq  5590  iss  6027  poirr2  6118  xp11  6167  nordeq  6380  nsuceq0  6447  ordequn  6467  fnbrfvb  6933  2f1fvneq  7262  foeqcnvco  7306  f1eqcocnv  7307  dfwe2  7786  releldmdifi  8054  mposn  8112  poxp2  8153  poxp3  8160  poseq  8168  tfrlem15  8393  tz7.44-2  8408  tz7.48-1  8446  tz7.49  8448  oawordexr  8557  oewordi  8593  oeeulem  8603  nna0r  8611  nnawordex  8639  nnaordex  8640  nnaordex2  8641  oaabs  8650  oaabs2  8651  eldifsucnn  8666  elecex  8761  ectocld  8796  ecoptocl  8821  mapsnd  8907  eqeng  9006  difsnen  9071  fopwdom  9097  nneneq  9214  frfi  9269  elfiun  9415  ordiso  9503  ordtypelem7  9511  wemaplem2  9534  suc11reg  9613  inf3lem6  9627  noinfep  9654  cantnff  9668  cantnfp1lem2  9673  cantnfp1lem3  9674  cantnflem1  9683  cantnf  9687  ttrcltr  9710  r111  9775  rankc2  9881  tcrank  9894  cardnueq0  10038  fodomfi2  10132  alephinit  10167  dfac9  10208  dfac12k  10219  djuinf  10260  ackbij1  10308  ackbij2  10313  sornom  10348  fin23lem16  10406  fin23lem21  10410  isf32lem2  10425  fin1a2lem6  10476  itunitc  10492  zorn2lem4  10570  wunr1om  10797  tskr1om  10845  recmulnq  11042  ltexnq  11053  distrlem4pr  11104  1re  11301  0re  11303  0cnALT  11538  0cnALT2  11539  mulge0  11827  prodgt0  12157  peano2nn  12340  recnz  12767  zneo  12775  uzn0  12975  xlemul1a  13411  prunioo  13605  flidz  13943  ceilidz  13985  modid2  14031  modmuladdnn0  14051  om2uzrani  14088  uzrdgfni  14094  seqid  14183  seqz  14186  facdiv  14424  facwordi  14426  hashdom  14516  wrdnval  14683  wrdnfi  14686  wrdl1s1  14755  sqrmo  15411  fsumf1o  15882  isumltss  16010  supcvg  16018  dvdsnegb  16436  dvdsexp2im  16490  odd2np1lem  16503  odd2np1  16504  ltoddhalfle  16524  halfleoddlt  16525  opoe  16526  omoe  16527  opeo  16528  omeo  16529  bitsuz  16637  bezoutlem4  16708  gcddiv  16717  gcdzeq  16718  dvdssqim  16720  dvdsexpim  16721  lcmgcdeq  16780  coprmdvds2  16822  rpmul  16827  divgcdcoprmex  16834  cncongr2  16836  dvdsprm  16872  coprm  16880  prmdvdsexp  16884  prmdiv  16955  pythagtriplem19  17004  pc2dvds  17050  pcadd  17060  prmpwdvds  17075  vdwlem11  17162  ramubcl  17189  0ram  17191  posasymb  18486  pleval2  18502  pltval3  18504  plttr  18507  pospo  18510  letsr  18760  intopsn  18825  ismgmid  18838  imasmgm2  18856  imasmnd2  18961  isgrpid2  19180  isgrpinv  19197  dfgrp3lem  19241  imasgrp2  19258  orbsta  19520  symgfix2  19623  pmtrfrn  19665  pmtrrn2  19667  odmulg  19763  odmulgeq  19764  gexdvdsi  19790  gexnnod  19795  pgpssslw  19821  sylow2alem1  19824  fislw  19832  lsmss1b  19873  lsmss2b  19875  efgrelexlemb  19957  torsubg  20061  ablfacrplem  20274  pgpfac1lem2  20284  pgpfac1lem3  20286  ablsimpnosubgd  20313  imasrng  20392  imasring  20553  dvdsrcl2  20589  dvdsrtr  20591  dvdsrmul1  20592  irredn0  20646  lspsneq0  21280  lmhmima  21315  lspsolv  21414  rspprop  21517  xrsdsreclblem  21712  dvdsrzring  21760  prmirredlem  21771  znunit  21862  pjdm2  22010  obselocv  22027  lindfrn  22120  opsrtoslem2  22358  mpfind  22417  psdmul  22480  mpfpf1  22662  pf1mpf  22663  cpmadugsumlemF  23187  baspartn  23265  bastop  23292  iscld3  23375  isopn3  23377  iscldtop  23406  ordtrest2lem  23514  2ndcredom  23761  2ndc1stc  23762  2ndcrest  23765  2ndcdisj  23768  2ndcsep  23771  kgenidm  23859  dfac14  23930  tx2ndc  23963  kqreglem1  24053  rnelfm  24265  fmfnfmlem2  24267  fmfnfmlem4  24269  fmfnfm  24270  flimtopon  24282  fclstopon  24324  xrsmopn  25125  icccmplem2  25136  reconnlem1  25139  iccpnfcnv  25258  cphsqrtcl2  25500  ivthlem3  25767  ivthicc  25772  ovolctb  25804  ioombl  25879  itgabs  26148  itgsplitioo  26151  dvlip  26306  c1liplem1  26309  c1lip1  26310  dvgt0lem1  26315  dvivthlem2  26322  dvne0  26324  lhop1lem  26326  lhop1  26327  lhop2  26328  lhop  26329  dvcvx  26333  itgsubstlem  26361  mdegnn0cl  26382  ig1peu  26486  elply2  26507  plypf1  26524  dgreq0  26577  aannenlem3  26650  abelthlem2  26752  lognegb  26911  eflogeq  26923  efopn  26979  cxpge0  27004  cxplea  27017  cxple2  27018  cxpcn3lem  27068  cxpaddlelem  27072  cxpaddle  27073  cxpeq  27078  asinsinb  27218  acoscosb  27219  atantanb  27245  wilthlem2  27389  sqf11  27459  sqff1o  27502  ppiublem1  27522  lgsdir  27652  lgsne0  27655  lgsquadlem3  27702  2sqblem  27751  dchrisum0flblem1  27828  ostth3  27958  ostth  27959  flt0  27962  fltoprm  27988  noseponlem  28014  nodenselem4  28037  nodenselem5  28038  nodenselem7  28040  nodenselem8  28041  nolt02o  28045  nogt01o  28046  nosupbnd2lem1  28065  noetasuplem4  28086  lesrec  28178  madebdayim  28267  negsproplem2  28408  negsunif  28434  negleft  28437  negright  28438  lemuls1ad  28561  precsexlem6  28591  precsexlem7  28592  noseqp1  28670  om2noseqlt  28678  noseqrdgfn  28685  bdayn0sf1o  28749  dfnns2  28751  bdayfinbndlem1  28846  colinearalg  29481  axcontlem5  29539  axcontlem9  29543  uhgrn0  29638  upgrfn  29658  umgrfn  29670  uvtxnbgrvtx  29967  vtxduhgr0nedg  30066  pthdivtx  30305  iswwlksnx  30422  wpthswwlks2on  30546  clwwlkn  30610  clwwlknonwwlknonb  30690  eupth2lem2  30813  eupth2lem3lem6  30827  htthlem  31512  pjpreeq  31993  h1dn0  32147  spansneleqi  32164  rnbra  32702  dfpjop  32777  elpjrn  32785  stm1i  32838  mdbr2  32891  mdsl2i  32917  sumdmdlem  33013  dmdbr6ati  33018  ordtrest2NEWlem  34547  xrge0iifcnv  34558  eulerpartlemb  34993  onvf1odlem4  35868  erdszelem8  35942  cvmlift3lem4  36066  cvmlift3lem5  36067  fmlasucdisj  36143  mrsub0  36260  mrsubccat  36262  mrsubcn  36263  msubrn  36273  msrid  36289  elmthm  36320  dfon2lem9  36533  btwnconn1lem11  36842  broutsideof2  36867  opnbnd  37093  tailfb  37145  tr0elw  37252  tr0el  37253  bj-ideqg1  38065  fin2so  38510  lindsadd  38516  poimirlem9  38527  poimirlem17  38535  poimirlem26  38544  poimirlem27  38545  poimirlem31  38549  itgabsnc  38587  ftc2nc  38600  sdclem2  38656  subspopn  38666  equivtotbnd  38692  rngosn3  38838  igenval2  38980  isfldidl  38982  relcnveq3  39239  iss2  39256  elrelscnveq3  39539  lshpinN  40026  lsatcv0eq  40084  lsatcv1  40085  cvrnbtwn3  40313  cvrnbtwn4  40316  cvrcmp  40320  atnlt  40350  cvlexchb1  40367  2llnne2N  40445  atcvr0eq  40463  lnnat  40464  cvrat4  40480  ps-1  40514  3at  40527  llncmp  40559  llnnlt  40560  llncvrlpln2  40594  llncvrlpln  40595  lplncmp  40599  lplnnlt  40602  lplncvrlvol2  40652  lplncvrlvol  40653  lvolcmp  40654  lvolnltN  40655  dalempnes  40688  dalemqnet  40689  dalem-cly  40708  dalem44  40753  lncmp  40820  cdlemblem  40830  llnexch2N  40907  osumcllem4N  40996  pexmidlem1N  41007  lhp2atnle  41070  cdleme11dN  41299  cdleme20k  41356  cdleme21at  41365  cdleme21ct  41366  cdleme32e  41482  cdleme35f  41491  tendoex  42012  dochexmidlem1  42497  lcfrlem9  42587  mapd1o  42685  mapdindp3  42759  zndvdchrrhm  43003  elre0re  43285  mullt0b2d  43528  ismrc  43691  pellexlem1  43815  aomclem4  44043  dfac21  44052  lsmfgcl  44060  lmhmfgima  44070  dfacbasgrp  44094  hbtlem6  44115  fiuneneq  44178  oaabsb  44280  cantnfresb  44310  orbitcl  45925  stoweidlem27  47006  stoweidlem29  47008  fcoresf1  48108  tz6.12c-afv2  48281  dfatbrafv2b  48284  fnbrafv2b  48287  iccpartrn  48481  prmdvdsfmtnof1lem2  48639  mod42tp1mod8  48656  isubgredg  48933  grimuhgr  48954  grimcnv  48955  isuspgrim0  48961  assintopass  49280  rrxsphere  49829