Theorem syl5ibcom 246

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  biimpcd  250  elrab3t  3635  mob2  3663  rmob  3829  sneqrg  4777  preq1b  4784  prel12g  4802  disjxun  5077  sotric  5563  sotrieq  5564  iss  5994  poirr2  6081  xp11  6133  nordeq  6336  nsuceq0  6402  ordequn  6422  fnbrfvb  6884  2f1fvneq  7211  foeqcnvco  7251  f1eqcocnv  7252  dfwe2  7724  releldmdifi  7994  mposn  8049  poxp2  8090  poxp3  8097  poseq  8105  tfrlem15  8328  tz7.44-2  8343  tz7.48-1  8379  tz7.49  8381  oawordexr  8488  oewordi  8524  oeeulem  8534  nna0r  8542  nnawordex  8570  nnaordex  8571  nnaordex2  8572  oaabs  8581  oaabs2  8582  eldifsucnn  8597  elecex  8691  ectocld  8726  ecoptocl  8751  mapsnd  8831  eqeng  8930  difsnen  8994  fopwdom  9020  nneneq  9137  frfi  9192  elfiun  9340  ordiso  9428  ordtypelem7  9436  wemaplem2  9459  suc11reg  9538  inf3lem6  9552  noinfep  9579  cantnff  9593  cantnfp1lem2  9598  cantnfp1lem3  9599  cantnflem1  9608  cantnf  9612  ttrcltr  9635  r111  9697  rankc2  9793  tcrank  9806  cardnueq0  9886  fodomfi2  9980  alephinit  10015  dfac9  10057  dfac12k  10068  djuinf  10109  ackbij1  10157  ackbij2  10162  sornom  10197  fin23lem16  10255  fin23lem21  10259  isf32lem2  10274  fin1a2lem6  10325  itunitc  10341  zorn2lem4  10419  wunr1om  10640  tskr1om  10688  recmulnq  10885  ltexnq  10896  distrlem4pr  10947  1re  11142  0re  11144  0cnALT  11379  0cnALT2  11380  mulge0  11666  prodgt0  12000  peano2nn  12184  recnz  12602  zneo  12610  uzn0  12803  xlemul1a  13238  prunioo  13432  flidz  13767  ceilidz  13809  modid2  13855  modmuladdnn0  13875  om2uzrani  13912  uzrdgfni  13918  seqid  14007  seqz  14010  facdiv  14247  facwordi  14249  hashdom  14339  wrdnval  14505  wrdnfi  14508  wrdl1s1  14575  sqrmo  15211  fsumf1o  15683  isumltss  15811  supcvg  15819  dvdsnegb  16240  dvdsexp2im  16294  odd2np1lem  16307  odd2np1  16308  ltoddhalfle  16328  halfleoddlt  16329  opoe  16330  omoe  16331  opeo  16332  omeo  16333  bitsuz  16441  bezoutlem4  16509  gcddiv  16518  gcdzeq  16519  dvdssqim  16521  dvdsexpim  16522  lcmgcdeq  16579  coprmdvds2  16621  rpmul  16626  divgcdcoprmex  16633  cncongr2  16635  dvdsprm  16671  coprm  16679  prmdvdsexp  16683  prmdiv  16753  pythagtriplem19  16802  pc2dvds  16848  pcadd  16858  prmpwdvds  16873  vdwlem11  16960  ramubcl  16987  0ram  16989  posasymb  18283  pleval2  18299  pltval3  18301  plttr  18304  pospo  18307  letsr  18557  intopsn  18620  ismgmid  18631  imasmnd2  18740  isgrpid2  18950  isgrpinv  18967  dfgrp3lem  19012  imasgrp2  19029  orbsta  19286  symgfix2  19389  pmtrfrn  19431  pmtrrn2  19433  odmulg  19529  odmulgeq  19530  gexdvdsi  19556  gexnnod  19561  pgpssslw  19587  sylow2alem1  19590  fislw  19598  lsmss1b  19639  lsmss2b  19641  efgrelexlemb  19723  torsubg  19827  ablfacrplem  20040  pgpfac1lem2  20050  pgpfac1lem3  20052  ablsimpnosubgd  20079  imasrng  20156  imasring  20308  dvdsrcl2  20344  dvdsrtr  20346  dvdsrmul1  20347  irredn0  20401  lspsneq0  21009  lmhmima  21044  lspsolv  21143  xrsdsreclblem  21395  dvdsrzring  21443  prmirredlem  21454  znunit  21545  pjdm2  21693  obselocv  21710  lindfrn  21803  opsrtoslem2  22039  mpfind  22098  psdmul  22161  mpfpf1  22344  pf1mpf  22345  cpmadugsumlemF  22866  baspartn  22944  bastop  22971  iscld3  23054  isopn3  23056  iscldtop  23085  ordtrest2lem  23193  2ndcredom  23440  2ndc1stc  23441  2ndcrest  23444  2ndcdisj  23446  2ndcsep  23449  kgenidm  23537  dfac14  23608  tx2ndc  23641  kqreglem1  23731  rnelfm  23943  fmfnfmlem2  23945  fmfnfmlem4  23947  fmfnfm  23948  flimtopon  23960  fclstopon  24002  xrsmopn  24803  icccmplem2  24814  reconnlem1  24817  iccpnfcnv  24936  cphsqrtcl2  25178  ivthlem3  25445  ivthicc  25450  ovolctb  25482  ioombl  25557  itgabs  25827  itgsplitioo  25830  dvlip  25985  c1liplem1  25988  c1lip1  25989  dvgt0lem1  25994  dvivthlem2  26001  dvne0  26003  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  dvcvx  26012  itgsubstlem  26040  mdegnn0cl  26061  ig1peu  26165  elply2  26186  plypf1  26202  dgreq0  26255  aannenlem3  26321  abelthlem2  26422  lognegb  26579  eflogeq  26591  efopn  26647  cxpge0  26672  cxplea  26685  cxple2  26686  cxpcn3lem  26736  cxpaddlelem  26740  cxpaddle  26741  cxpeq  26746  asinsinb  26886  acoscosb  26887  atantanb  26913  wilthlem2  27057  sqf11  27127  sqff1o  27170  ppiublem1  27190  lgsdir  27320  lgsne0  27323  lgsquadlem3  27370  2sqblem  27419  dchrisum0flblem1  27496  ostth3  27626  ostth  27627  noseponlem  27653  nodenselem4  27676  nodenselem5  27677  nodenselem7  27679  nodenselem8  27680  nolt02o  27684  nogt01o  27685  nosupbnd2lem1  27704  noetasuplem4  27725  lesrec  27816  madebdayim  27905  negsproplem2  28046  negsunif  28072  negleft  28075  negright  28076  lemuls1ad  28199  precsexlem6  28229  precsexlem7  28230  noseqp1  28308  om2noseqlt  28316  noseqrdgfn  28323  bdayn0sf1o  28387  dfnns2  28389  bdayfinbndlem1  28484  colinearalg  29004  axcontlem5  29062  axcontlem9  29066  uhgrn0  29161  upgrfn  29181  umgrfn  29193  uvtxnbgrvtx  29487  vtxduhgr0nedg  29586  pthdivtx  29820  iswwlksnx  29933  wpthswwlks2on  30057  clwwlkn  30121  clwwlknonwwlknonb  30201  eupth2lem2  30314  eupth2lem3lem6  30328  htthlem  31013  pjpreeq  31494  h1dn0  31648  spansneleqi  31665  rnbra  32203  dfpjop  32278  elpjrn  32286  stm1i  32339  mdbr2  32392  mdsl2i  32418  sumdmdlem  32514  dmdbr6ati  32519  ordtrest2NEWlem  34113  xrge0iifcnv  34124  eulerpartlemb  34559  onvf1odlem4  35341  erdszelem8  35433  cvmlift3lem4  35557  cvmlift3lem5  35558  fmlasucdisj  35634  mrsub0  35751  mrsubccat  35753  mrsubcn  35754  msubrn  35764  msrid  35780  elmthm  35811  dfon2lem9  36024  btwnconn1lem11  36332  broutsideof2  36357  opnbnd  36560  tailfb  36612  tr0elw  36719  tr0el  36720  bj-ideqg1  37531  fin2so  37981  lindsadd  37987  poimirlem9  38003  poimirlem17  38011  poimirlem26  38020  poimirlem27  38021  poimirlem31  38025  itgabsnc  38063  ftc2nc  38076  sdclem2  38116  subspopn  38126  equivtotbnd  38152  rngosn3  38298  igenval2  38440  isfldidl  38442  relcnveq3  38701  iss2  38718  elrelscnveq3  39001  lshpinN  39488  lsatcv0eq  39546  lsatcv1  39547  cvrnbtwn3  39775  cvrnbtwn4  39778  cvrcmp  39782  atnlt  39812  cvlexchb1  39829  2llnne2N  39907  atcvr0eq  39925  lnnat  39926  cvrat4  39942  ps-1  39976  3at  39989  llncmp  40021  llnnlt  40022  llncvrlpln2  40056  llncvrlpln  40057  lplncmp  40061  lplnnlt  40064  lplncvrlvol2  40114  lplncvrlvol  40115  lvolcmp  40116  lvolnltN  40117  dalempnes  40150  dalemqnet  40151  dalem-cly  40170  dalem44  40215  lncmp  40282  cdlemblem  40292  llnexch2N  40369  osumcllem4N  40458  pexmidlem1N  40469  lhp2atnle  40532  cdleme11dN  40761  cdleme20k  40818  cdleme21at  40827  cdleme21ct  40828  cdleme32e  40944  cdleme35f  40953  tendoex  41474  dochexmidlem1  41959  lcfrlem9  42049  mapd1o  42147  mapdindp3  42221  zndvdchrrhm  42465  elre0re  42745  mullt0b2d  42981  flt0  43094  ismrc  43157  pellexlem1  43281  aomclem4  43509  dfac21  43518  lsmfgcl  43526  lmhmfgima  43536  dfacbasgrp  43560  hbtlem6  43581  fiuneneq  43644  oaabsb  43746  cantnfresb  43776  orbitcl  45408  stoweidlem27  46477  stoweidlem29  46479  fcoresf1  47539  tz6.12c-afv2  47712  dfatbrafv2b  47715  fnbrafv2b  47718  iccpartrn  47912  prmdvdsfmtnof1lem2  48070  mod42tp1mod8  48087  isubgredg  48364  grimuhgr  48385  grimcnv  48386  isuspgrim0  48392  assintopass  48712  rrxsphere  49246