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  3652  mob2  3681  rmob  3846  sneqrg  4799  preq1b  4806  prel12g  4824  disjxun  5102  sotric  5589  sotrieq  5590  iss  6027  poirr2  6114  xp11  6164  nordeq  6368  nsuceq0  6435  ordequn  6455  fnbrfvb  6921  2f1fvneq  7248  foeqcnvco  7288  f1eqcocnv  7289  dfwe2  7761  releldmdifi  8030  mposn  8086  poxp2  8127  poxp3  8134  poseq  8142  tfrlem15  8367  tz7.44-2  8382  tz7.48-1  8418  tz7.49  8420  oawordexr  8529  oewordi  8565  oeeulem  8575  nna0r  8583  nnawordex  8611  nnaordex  8612  nnaordex2  8613  oaabs  8622  oaabs2  8623  eldifsucnn  8638  elecex  8733  ectocld  8768  ecoptocl  8793  mapsnd  8872  eqeng  8971  difsnen  9035  fopwdom  9061  nneneq  9178  frfi  9233  elfiun  9378  ordiso  9466  ordtypelem7  9474  wemaplem2  9497  suc11reg  9576  inf3lem6  9590  noinfep  9617  cantnff  9631  cantnfp1lem2  9636  cantnfp1lem3  9637  cantnflem1  9646  cantnf  9650  ttrcltr  9673  r111  9735  rankc2  9831  tcrank  9844  cardnueq0  9938  fodomfi2  10032  alephinit  10067  dfac9  10108  dfac12k  10119  djuinf  10160  ackbij1  10208  ackbij2  10213  sornom  10249  fin23lem16  10307  fin23lem21  10311  isf32lem2  10326  fin1a2lem6  10377  itunitc  10393  zorn2lem4  10471  wunr1om  10692  tskr1om  10740  recmulnq  10937  ltexnq  10948  distrlem4pr  10999  1re  11196  0re  11198  0cnALT  11433  0cnALT2  11434  mulge0  11720  prodgt0  12050  peano2nn  12233  recnz  12659  zneo  12667  uzn0  12867  xlemul1a  13302  prunioo  13496  flidz  13831  ceilidz  13873  modid2  13919  modmuladdnn0  13939  om2uzrani  13976  uzrdgfni  13982  seqid  14071  seqz  14074  facdiv  14311  facwordi  14313  hashdom  14403  wrdnval  14570  wrdnfi  14573  wrdl1s1  14640  sqrmo  15290  fsumf1o  15762  isumltss  15890  supcvg  15898  dvdsnegb  16319  dvdsexp2im  16373  odd2np1lem  16386  odd2np1  16387  ltoddhalfle  16407  halfleoddlt  16408  opoe  16409  omoe  16410  opeo  16411  omeo  16412  bitsuz  16520  bezoutlem4  16588  gcddiv  16597  gcdzeq  16598  dvdssqim  16600  dvdsexpim  16601  lcmgcdeq  16658  coprmdvds2  16700  rpmul  16705  divgcdcoprmex  16712  cncongr2  16714  dvdsprm  16750  coprm  16758  prmdvdsexp  16762  prmdiv  16832  pythagtriplem19  16881  pc2dvds  16927  pcadd  16937  prmpwdvds  16952  vdwlem11  17039  ramubcl  17066  0ram  17068  posasymb  18363  pleval2  18379  pltval3  18381  plttr  18384  pospo  18387  letsr  18637  intopsn  18700  ismgmid  18711  imasmnd2  18820  isgrpid2  19031  isgrpinv  19048  dfgrp3lem  19092  imasgrp2  19109  orbsta  19371  symgfix2  19474  pmtrfrn  19516  pmtrrn2  19518  odmulg  19614  odmulgeq  19615  gexdvdsi  19641  gexnnod  19646  pgpssslw  19672  sylow2alem1  19675  fislw  19683  lsmss1b  19724  lsmss2b  19726  efgrelexlemb  19808  torsubg  19912  ablfacrplem  20125  pgpfac1lem2  20135  pgpfac1lem3  20137  ablsimpnosubgd  20164  imasrng  20243  imasring  20400  dvdsrcl2  20436  dvdsrtr  20438  dvdsrmul1  20439  irredn0  20493  lspsneq0  21099  lmhmima  21134  lspsolv  21233  xrsdsreclblem  21520  dvdsrzring  21568  prmirredlem  21579  znunit  21670  pjdm2  21818  obselocv  21835  lindfrn  21928  opsrtoslem2  22164  mpfind  22223  psdmul  22286  mpfpf1  22468  pf1mpf  22469  cpmadugsumlemF  22990  baspartn  23068  bastop  23095  iscld3  23178  isopn3  23180  iscldtop  23209  ordtrest2lem  23317  2ndcredom  23564  2ndc1stc  23565  2ndcrest  23568  2ndcdisj  23570  2ndcsep  23573  kgenidm  23661  dfac14  23732  tx2ndc  23765  kqreglem1  23855  rnelfm  24067  fmfnfmlem2  24069  fmfnfmlem4  24071  fmfnfm  24072  flimtopon  24084  fclstopon  24126  xrsmopn  24927  icccmplem2  24938  reconnlem1  24941  iccpnfcnv  25060  cphsqrtcl2  25302  ivthlem3  25569  ivthicc  25574  ovolctb  25606  ioombl  25681  itgabs  25951  itgsplitioo  25954  dvlip  26109  c1liplem1  26112  c1lip1  26113  dvgt0lem1  26118  dvivthlem2  26125  dvne0  26127  lhop1lem  26129  lhop1  26130  lhop2  26131  lhop  26132  dvcvx  26136  itgsubstlem  26164  mdegnn0cl  26185  ig1peu  26289  elply2  26310  plypf1  26326  dgreq0  26379  aannenlem3  26448  abelthlem2  26549  lognegb  26709  eflogeq  26721  efopn  26777  cxpge0  26802  cxplea  26815  cxple2  26816  cxpcn3lem  26866  cxpaddlelem  26870  cxpaddle  26871  cxpeq  26876  asinsinb  27016  acoscosb  27017  atantanb  27043  wilthlem2  27187  sqf11  27257  sqff1o  27300  ppiublem1  27320  lgsdir  27450  lgsne0  27453  lgsquadlem3  27500  2sqblem  27549  dchrisum0flblem1  27626  ostth3  27756  ostth  27757  noseponlem  27782  nodenselem4  27805  nodenselem5  27806  nodenselem7  27808  nodenselem8  27809  nolt02o  27813  nogt01o  27814  nosupbnd2lem1  27833  noetasuplem4  27854  lesrec  27946  madebdayim  28035  negsproplem2  28176  negsunif  28202  negleft  28205  negright  28206  lemuls1ad  28329  precsexlem6  28359  precsexlem7  28360  noseqp1  28438  om2noseqlt  28446  noseqrdgfn  28453  bdayn0sf1o  28517  dfnns2  28519  bdayfinbndlem1  28614  colinearalg  29165  axcontlem5  29223  axcontlem9  29227  uhgrn0  29322  upgrfn  29342  umgrfn  29354  uvtxnbgrvtx  29648  vtxduhgr0nedg  29747  pthdivtx  29981  iswwlksnx  30094  wpthswwlks2on  30218  clwwlkn  30282  clwwlknonwwlknonb  30362  eupth2lem2  30475  eupth2lem3lem6  30489  htthlem  31174  pjpreeq  31655  h1dn0  31809  spansneleqi  31826  rnbra  32364  dfpjop  32439  elpjrn  32447  stm1i  32500  mdbr2  32553  mdsl2i  32579  sumdmdlem  32675  dmdbr6ati  32680  ordtrest2NEWlem  34224  xrge0iifcnv  34235  eulerpartlemb  34670  onvf1odlem4  35456  erdszelem8  35556  cvmlift3lem4  35680  cvmlift3lem5  35681  fmlasucdisj  35757  mrsub0  35874  mrsubccat  35876  mrsubcn  35877  msubrn  35887  msrid  35903  elmthm  35934  dfon2lem9  36147  btwnconn1lem11  36455  broutsideof2  36480  opnbnd  36693  tailfb  36745  tr0elw  36852  tr0el  36853  bj-ideqg1  37663  fin2so  38113  lindsadd  38119  poimirlem9  38135  poimirlem17  38143  poimirlem26  38152  poimirlem27  38153  poimirlem31  38157  itgabsnc  38195  ftc2nc  38208  sdclem2  38248  subspopn  38258  equivtotbnd  38284  rngosn3  38430  igenval2  38572  isfldidl  38574  relcnveq3  38833  iss2  38850  elrelscnveq3  39133  lshpinN  39620  lsatcv0eq  39678  lsatcv1  39679  cvrnbtwn3  39907  cvrnbtwn4  39910  cvrcmp  39914  atnlt  39944  cvlexchb1  39961  2llnne2N  40039  atcvr0eq  40057  lnnat  40058  cvrat4  40074  ps-1  40108  3at  40121  llncmp  40153  llnnlt  40154  llncvrlpln2  40188  llncvrlpln  40189  lplncmp  40193  lplnnlt  40196  lplncvrlvol2  40246  lplncvrlvol  40247  lvolcmp  40248  lvolnltN  40249  dalempnes  40282  dalemqnet  40283  dalem-cly  40302  dalem44  40347  lncmp  40414  cdlemblem  40424  llnexch2N  40501  osumcllem4N  40590  pexmidlem1N  40601  lhp2atnle  40664  cdleme11dN  40893  cdleme20k  40950  cdleme21at  40959  cdleme21ct  40960  cdleme32e  41076  cdleme35f  41085  tendoex  41606  dochexmidlem1  42091  lcfrlem9  42181  mapd1o  42279  mapdindp3  42353  zndvdchrrhm  42597  elre0re  42877  mullt0b2d  43113  flt0  43226  ismrc  43289  pellexlem1  43413  aomclem4  43641  dfac21  43650  lsmfgcl  43658  lmhmfgima  43668  dfacbasgrp  43692  hbtlem6  43713  fiuneneq  43776  oaabsb  43878  cantnfresb  43908  orbitcl  45525  stoweidlem27  46600  stoweidlem29  46602  fcoresf1  47662  tz6.12c-afv2  47835  dfatbrafv2b  47838  fnbrafv2b  47841  iccpartrn  48035  prmdvdsfmtnof1lem2  48193  mod42tp1mod8  48210  isubgredg  48487  grimuhgr  48508  grimcnv  48509  isuspgrim0  48515  assintopass  48835  rrxsphere  49380