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  5593  sotrieq  5594  iss  6031  poirr2  6118  xp11  6168  nordeq  6376  nsuceq0  6443  ordequn  6463  fnbrfvb  6928  2f1fvneq  7257  foeqcnvco  7301  f1eqcocnv  7302  dfwe2  7773  releldmdifi  8042  mposn  8100  poxp2  8141  poxp3  8148  poseq  8156  tfrlem15  8381  tz7.44-2  8396  tz7.48-1  8432  tz7.49  8434  oawordexr  8543  oewordi  8579  oeeulem  8589  nna0r  8597  nnawordex  8625  nnaordex  8626  nnaordex2  8627  oaabs  8636  oaabs2  8637  eldifsucnn  8652  elecex  8747  ectocld  8782  ecoptocl  8807  mapsnd  8893  eqeng  8992  difsnen  9057  fopwdom  9083  nneneq  9200  frfi  9255  elfiun  9400  ordiso  9488  ordtypelem7  9496  wemaplem2  9519  suc11reg  9598  inf3lem6  9612  noinfep  9639  cantnff  9653  cantnfp1lem2  9658  cantnfp1lem3  9659  cantnflem1  9668  cantnf  9672  ttrcltr  9695  r111  9757  rankc2  9853  tcrank  9866  cardnueq0  9969  fodomfi2  10063  alephinit  10098  dfac9  10139  dfac12k  10150  djuinf  10191  ackbij1  10239  ackbij2  10244  sornom  10279  fin23lem16  10337  fin23lem21  10341  isf32lem2  10356  fin1a2lem6  10407  itunitc  10423  zorn2lem4  10501  wunr1om  10728  tskr1om  10776  recmulnq  10973  ltexnq  10984  distrlem4pr  11035  1re  11232  0re  11234  0cnALT  11469  0cnALT2  11470  mulge0  11756  prodgt0  12086  peano2nn  12269  recnz  12696  zneo  12704  uzn0  12904  xlemul1a  13340  prunioo  13534  flidz  13871  ceilidz  13913  modid2  13959  modmuladdnn0  13979  om2uzrani  14016  uzrdgfni  14022  seqid  14111  seqz  14114  facdiv  14351  facwordi  14353  hashdom  14443  wrdnval  14610  wrdnfi  14613  wrdl1s1  14682  sqrmo  15338  fsumf1o  15809  isumltss  15937  supcvg  15945  dvdsnegb  16363  dvdsexp2im  16417  odd2np1lem  16430  odd2np1  16431  ltoddhalfle  16451  halfleoddlt  16452  opoe  16453  omoe  16454  opeo  16455  omeo  16456  bitsuz  16564  bezoutlem4  16632  gcddiv  16641  gcdzeq  16642  dvdssqim  16644  dvdsexpim  16645  lcmgcdeq  16702  coprmdvds2  16744  rpmul  16749  divgcdcoprmex  16756  cncongr2  16758  dvdsprm  16794  coprm  16802  prmdvdsexp  16806  prmdiv  16876  pythagtriplem19  16925  pc2dvds  16971  pcadd  16981  prmpwdvds  16996  vdwlem11  17083  ramubcl  17110  0ram  17112  posasymb  18407  pleval2  18423  pltval3  18425  plttr  18428  pospo  18431  letsr  18681  intopsn  18746  ismgmid  18758  imasmgm2  18776  imasmnd2  18881  isgrpid2  19100  isgrpinv  19117  dfgrp3lem  19161  imasgrp2  19178  orbsta  19440  symgfix2  19543  pmtrfrn  19585  pmtrrn2  19587  odmulg  19683  odmulgeq  19684  gexdvdsi  19710  gexnnod  19715  pgpssslw  19741  sylow2alem1  19744  fislw  19752  lsmss1b  19793  lsmss2b  19795  efgrelexlemb  19877  torsubg  19981  ablfacrplem  20194  pgpfac1lem2  20204  pgpfac1lem3  20206  ablsimpnosubgd  20233  imasrng  20312  imasring  20471  dvdsrcl2  20507  dvdsrtr  20509  dvdsrmul1  20510  irredn0  20564  lspsneq0  21196  lmhmima  21231  lspsolv  21330  rspprop  21433  xrsdsreclblem  21626  dvdsrzring  21674  prmirredlem  21685  znunit  21776  pjdm2  21924  obselocv  21941  lindfrn  22034  opsrtoslem2  22272  mpfind  22331  psdmul  22394  mpfpf1  22576  pf1mpf  22577  cpmadugsumlemF  23101  baspartn  23179  bastop  23206  iscld3  23289  isopn3  23291  iscldtop  23320  ordtrest2lem  23428  2ndcredom  23675  2ndc1stc  23676  2ndcrest  23679  2ndcdisj  23682  2ndcsep  23685  kgenidm  23773  dfac14  23844  tx2ndc  23877  kqreglem1  23967  rnelfm  24179  fmfnfmlem2  24181  fmfnfmlem4  24183  fmfnfm  24184  flimtopon  24196  fclstopon  24238  xrsmopn  25039  icccmplem2  25050  reconnlem1  25053  iccpnfcnv  25172  cphsqrtcl2  25414  ivthlem3  25681  ivthicc  25686  ovolctb  25718  ioombl  25793  itgabs  26062  itgsplitioo  26065  dvlip  26220  c1liplem1  26223  c1lip1  26224  dvgt0lem1  26229  dvivthlem2  26236  dvne0  26238  lhop1lem  26240  lhop1  26241  lhop2  26242  lhop  26243  dvcvx  26247  itgsubstlem  26275  mdegnn0cl  26296  ig1peu  26400  elply2  26421  plypf1  26438  dgreq0  26491  aannenlem3  26566  abelthlem2  26668  lognegb  26827  eflogeq  26839  efopn  26895  cxpge0  26920  cxplea  26933  cxple2  26934  cxpcn3lem  26984  cxpaddlelem  26988  cxpaddle  26989  cxpeq  26994  asinsinb  27134  acoscosb  27135  atantanb  27161  wilthlem2  27305  sqf11  27375  sqff1o  27418  ppiublem1  27438  lgsdir  27568  lgsne0  27571  lgsquadlem3  27618  2sqblem  27667  dchrisum0flblem1  27744  ostth3  27874  ostth  27875  noseponlem  27900  nodenselem4  27923  nodenselem5  27924  nodenselem7  27926  nodenselem8  27927  nolt02o  27931  nogt01o  27932  nosupbnd2lem1  27951  noetasuplem4  27972  lesrec  28064  madebdayim  28153  negsproplem2  28294  negsunif  28320  negleft  28323  negright  28324  lemuls1ad  28447  precsexlem6  28477  precsexlem7  28478  noseqp1  28556  om2noseqlt  28564  noseqrdgfn  28571  bdayn0sf1o  28635  dfnns2  28637  bdayfinbndlem1  28732  colinearalg  29367  axcontlem5  29425  axcontlem9  29429  uhgrn0  29524  upgrfn  29544  umgrfn  29556  uvtxnbgrvtx  29853  vtxduhgr0nedg  29952  pthdivtx  30191  iswwlksnx  30308  wpthswwlks2on  30432  clwwlkn  30496  clwwlknonwwlknonb  30576  eupth2lem2  30699  eupth2lem3lem6  30713  htthlem  31398  pjpreeq  31879  h1dn0  32033  spansneleqi  32050  rnbra  32588  dfpjop  32663  elpjrn  32671  stm1i  32724  mdbr2  32777  mdsl2i  32803  sumdmdlem  32899  dmdbr6ati  32904  ordtrest2NEWlem  34432  xrge0iifcnv  34443  eulerpartlemb  34879  onvf1odlem4  35703  erdszelem8  35777  cvmlift3lem4  35901  cvmlift3lem5  35902  fmlasucdisj  35978  mrsub0  36095  mrsubccat  36097  mrsubcn  36098  msubrn  36108  msrid  36124  elmthm  36155  dfon2lem9  36368  btwnconn1lem11  36677  broutsideof2  36702  opnbnd  36944  tailfb  36996  tr0elw  37103  tr0el  37104  bj-ideqg1  37916  fin2so  38361  lindsadd  38367  poimirlem9  38378  poimirlem17  38386  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  itgabsnc  38438  ftc2nc  38451  sdclem2  38492  subspopn  38502  equivtotbnd  38528  rngosn3  38674  igenval2  38816  isfldidl  38818  relcnveq3  39075  iss2  39092  elrelscnveq3  39375  lshpinN  39862  lsatcv0eq  39920  lsatcv1  39921  cvrnbtwn3  40149  cvrnbtwn4  40152  cvrcmp  40156  atnlt  40186  cvlexchb1  40203  2llnne2N  40281  atcvr0eq  40299  lnnat  40300  cvrat4  40316  ps-1  40350  3at  40363  llncmp  40395  llnnlt  40396  llncvrlpln2  40430  llncvrlpln  40431  lplncmp  40435  lplnnlt  40438  lplncvrlvol2  40488  lplncvrlvol  40489  lvolcmp  40490  lvolnltN  40491  dalempnes  40524  dalemqnet  40525  dalem-cly  40544  dalem44  40589  lncmp  40656  cdlemblem  40666  llnexch2N  40743  osumcllem4N  40832  pexmidlem1N  40843  lhp2atnle  40906  cdleme11dN  41135  cdleme20k  41192  cdleme21at  41201  cdleme21ct  41202  cdleme32e  41318  cdleme35f  41327  tendoex  41848  dochexmidlem1  42333  lcfrlem9  42423  mapd1o  42521  mapdindp3  42595  zndvdchrrhm  42839  elre0re  43121  mullt0b2d  43372  flt0  43483  ismrc  43546  pellexlem1  43670  aomclem4  43898  dfac21  43907  lsmfgcl  43915  lmhmfgima  43925  dfacbasgrp  43949  hbtlem6  43970  fiuneneq  44033  oaabsb  44135  cantnfresb  44165  orbitcl  45780  stoweidlem27  46855  stoweidlem29  46857  fcoresf1  47957  tz6.12c-afv2  48130  dfatbrafv2b  48133  fnbrafv2b  48136  iccpartrn  48330  prmdvdsfmtnof1lem2  48488  mod42tp1mod8  48505  isubgredg  48782  grimuhgr  48803  grimcnv  48804  isuspgrim0  48810  assintopass  49129  rrxsphere  49678