Theorem syl5ibcom 245

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpcd  249  elrab3t  3658  mob2  3686  rmob  3853  sneqrg  4803  preq1b  4810  prel12g  4828  disjxun  5105  sotric  5576  sotrieq  5577  iss  6006  poirr2  6097  xp11  6148  nordeq  6351  nsuceq0  6417  ordequn  6437  tz6.12cOLD  6885  fnbrfvb  6911  2f1fvneq  7235  foeqcnvco  7275  f1eqcocnv  7276  dfwe2  7750  releldmdifi  8024  mposn  8082  poxp2  8122  poxp3  8129  poseq  8137  tfrlem15  8360  tz7.44-2  8375  tz7.48-1  8411  tz7.49  8413  oawordexr  8520  oewordi  8555  oeeulem  8565  nna0r  8573  nnawordex  8601  nnaordex  8602  nnaordex2  8603  oaabs  8612  oaabs2  8613  eldifsucnn  8628  elecex  8721  ectocld  8755  ecoptocl  8780  mapsnd  8859  eqeng  8957  difsnen  9023  fopwdom  9049  nneneq  9170  frfi  9232  elfiun  9381  ordiso  9469  ordtypelem7  9477  wemaplem2  9500  suc11reg  9572  inf3lem6  9586  noinfep  9613  cantnff  9627  cantnfp1lem2  9632  cantnfp1lem3  9633  cantnflem1  9642  cantnf  9646  ttrcltr  9669  r111  9728  rankc2  9824  tcrank  9837  cardnueq0  9917  fodomfi2  10013  alephinit  10048  dfac9  10090  dfac12k  10101  djuinf  10142  ackbij1  10190  ackbij2  10195  sornom  10230  fin23lem16  10288  fin23lem21  10292  isf32lem2  10307  fin1a2lem6  10358  itunitc  10374  zorn2lem4  10452  wunr1om  10672  tskr1om  10720  recmulnq  10917  ltexnq  10928  distrlem4pr  10979  1re  11174  0re  11176  0cnALT  11409  0cnALT2  11410  mulge0  11696  prodgt0  12029  peano2nn  12198  recnz  12609  zneo  12617  uzn0  12810  xlemul1a  13248  prunioo  13442  flidz  13772  ceilidz  13814  modid2  13860  modmuladdnn0  13880  om2uzrani  13917  uzrdgfni  13923  seqid  14012  seqz  14015  facdiv  14252  facwordi  14254  hashdom  14344  wrdnval  14510  wrdnfi  14513  wrdl1s1  14579  sqrmo  15217  fsumf1o  15689  isumltss  15814  supcvg  15822  dvdsnegb  16243  dvdsexp2im  16297  odd2np1lem  16310  odd2np1  16311  ltoddhalfle  16331  halfleoddlt  16332  opoe  16333  omoe  16334  opeo  16335  omeo  16336  bitsuz  16444  bezoutlem4  16512  gcddiv  16521  gcdzeq  16522  dvdssqim  16524  dvdsexpim  16525  lcmgcdeq  16582  coprmdvds2  16624  rpmul  16629  divgcdcoprmex  16636  cncongr2  16638  dvdsprm  16673  coprm  16681  prmdvdsexp  16685  prmdiv  16755  pythagtriplem19  16804  pc2dvds  16850  pcadd  16860  prmpwdvds  16875  vdwlem11  16962  ramubcl  16989  0ram  16991  posasymb  18280  pleval2  18296  pltval3  18298  plttr  18301  pospo  18304  letsr  18552  intopsn  18581  ismgmid  18592  imasmnd2  18701  isgrpid2  18908  isgrpinv  18925  dfgrp3lem  18970  imasgrp2  18987  orbsta  19245  symgfix2  19346  pmtrfrn  19388  pmtrrn2  19390  odmulg  19486  odmulgeq  19487  gexdvdsi  19513  gexnnod  19518  pgpssslw  19544  sylow2alem1  19547  fislw  19555  lsmss1b  19596  lsmss2b  19598  efgrelexlemb  19680  torsubg  19784  ablfacrplem  19997  pgpfac1lem2  20007  pgpfac1lem3  20009  ablsimpnosubgd  20036  imasrng  20086  imasring  20239  dvdsrcl2  20275  dvdsrtr  20277  dvdsrmul1  20278  irredn0  20332  lspsneq0  20918  lmhmima  20954  lspsolv  21053  xrsdsreclblem  21329  dvdsrzring  21371  prmirredlem  21382  znunit  21473  pjdm2  21620  obselocv  21637  lindfrn  21730  opsrtoslem2  21963  mpfind  22014  psdmul  22053  mpfpf1  22238  pf1mpf  22239  cpmadugsumlemF  22763  baspartn  22841  bastop  22868  iscld3  22951  isopn3  22953  iscldtop  22982  ordtrest2lem  23090  2ndcredom  23337  2ndc1stc  23338  2ndcrest  23341  2ndcdisj  23343  2ndcsep  23346  kgenidm  23434  dfac14  23505  tx2ndc  23538  kqreglem1  23628  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  fmfnfm  23845  flimtopon  23857  fclstopon  23899  xrsmopn  24701  icccmplem2  24712  reconnlem1  24715  iccpnfcnv  24842  cphsqrtcl2  25086  ivthlem3  25354  ivthicc  25359  ovolctb  25391  ioombl  25466  itgabs  25736  itgsplitioo  25739  dvlip  25898  c1liplem1  25901  c1lip1  25902  dvgt0lem1  25907  dvivthlem2  25914  dvne0  25916  lhop1lem  25918  lhop1  25919  lhop2  25920  lhop  25921  dvcvx  25925  itgsubstlem  25955  mdegnn0cl  25976  ig1peu  26080  elply2  26101  plypf1  26117  dgreq0  26171  aannenlem3  26238  abelthlem2  26342  lognegb  26499  eflogeq  26511  efopn  26567  cxpge0  26592  cxplea  26605  cxple2  26606  cxpcn3lem  26657  cxpaddlelem  26661  cxpaddle  26662  cxpeq  26667  asinsinb  26807  acoscosb  26808  atantanb  26834  wilthlem2  26979  sqf11  27049  sqff1o  27092  ppiublem1  27113  lgsdir  27243  lgsne0  27246  lgsquadlem3  27293  2sqblem  27342  dchrisum0flblem1  27419  ostth3  27549  ostth  27550  noseponlem  27576  nodenselem4  27599  nodenselem5  27600  nodenselem7  27602  nodenselem8  27603  nolt02o  27607  nogt01o  27608  nosupbnd2lem1  27627  noetasuplem4  27648  slerec  27731  madebdayim  27799  negsproplem2  27935  negsunif  27961  slemul1ad  28085  precsexlem6  28114  precsexlem7  28115  noseqp1  28185  om2noseqlt  28193  noseqrdgfn  28200  bdayn0sf1o  28259  dfnns2  28261  colinearalg  28837  axcontlem5  28895  axcontlem9  28899  uhgrn0  28994  upgrfn  29014  umgrfn  29026  uvtxnbgrvtx  29320  vtxduhgr0nedg  29420  pthdivtx  29657  iswwlksnx  29770  wpthswwlks2on  29891  clwwlkn  29955  clwwlknonwwlknonb  30035  eupth2lem2  30148  eupth2lem3lem6  30162  htthlem  30846  pjpreeq  31327  h1dn0  31481  spansneleqi  31498  rnbra  32036  dfpjop  32111  elpjrn  32119  stm1i  32172  mdbr2  32225  mdsl2i  32251  sumdmdlem  32347  dmdbr6ati  32352  ordtrest2NEWlem  33912  xrge0iifcnv  33923  eulerpartlemb  34359  onvf1odlem4  35093  erdszelem8  35185  cvmlift3lem4  35309  cvmlift3lem5  35310  fmlasucdisj  35386  mrsub0  35503  mrsubccat  35505  mrsubcn  35506  msubrn  35516  msrid  35532  elmthm  35563  dfon2lem9  35779  btwnconn1lem11  36085  broutsideof2  36110  opnbnd  36313  tailfb  36365  bj-ideqg1  37152  fin2so  37601  lindsadd  37607  poimirlem9  37623  poimirlem17  37631  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  itgabsnc  37683  ftc2nc  37696  sdclem2  37736  subspopn  37746  equivtotbnd  37772  rngosn3  37918  igenval2  38060  isfldidl  38062  relcnveq3  38309  iss2  38326  elrelscnveq3  38482  lshpinN  38982  lsatcv0eq  39040  lsatcv1  39041  cvrnbtwn3  39269  cvrnbtwn4  39272  cvrcmp  39276  atnlt  39306  cvlexchb1  39323  2llnne2N  39402  atcvr0eq  39420  lnnat  39421  cvrat4  39437  ps-1  39471  3at  39484  llncmp  39516  llnnlt  39517  llncvrlpln2  39551  llncvrlpln  39552  lplncmp  39556  lplnnlt  39559  lplncvrlvol2  39609  lplncvrlvol  39610  lvolcmp  39611  lvolnltN  39612  dalempnes  39645  dalemqnet  39646  dalem-cly  39665  dalem44  39710  lncmp  39777  cdlemblem  39787  llnexch2N  39864  osumcllem4N  39953  pexmidlem1N  39964  lhp2atnle  40027  cdleme11dN  40256  cdleme20k  40313  cdleme21at  40322  cdleme21ct  40323  cdleme32e  40439  cdleme35f  40448  tendoex  40969  dochexmidlem1  41454  lcfrlem9  41544  mapd1o  41642  mapdindp3  41716  zndvdchrrhm  41960  elre0re  42242  mullt0b2d  42472  flt0  42625  ismrc  42689  pellexlem1  42817  aomclem4  43046  dfac21  43055  lsmfgcl  43063  lmhmfgima  43073  dfacbasgrp  43097  hbtlem6  43118  fiuneneq  43181  oaabsb  43283  cantnfresb  43313  orbitcl  44947  stoweidlem27  46025  stoweidlem29  46027  fcoresf1  47070  tz6.12c-afv2  47243  dfatbrafv2b  47246  fnbrafv2b  47249  iccpartrn  47431  prmdvdsfmtnof1lem2  47586  mod42tp1mod8  47603  isubgredg  47866  grimuhgr  47887  grimcnv  47888  isuspgrim0  47894  assintopass  48202  rrxsphere  48737