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  3633  mob2  3661  rmob  3828  sneqrg  4782  preq1b  4789  prel12g  4807  disjxun  5083  sotric  5569  sotrieq  5570  iss  6000  poirr2  6087  xp11  6139  nordeq  6342  nsuceq0  6408  ordequn  6428  fnbrfvb  6890  2f1fvneq  7215  foeqcnvco  7255  f1eqcocnv  7256  dfwe2  7728  releldmdifi  7998  mposn  8053  poxp2  8093  poxp3  8100  poseq  8108  tfrlem15  8331  tz7.44-2  8346  tz7.48-1  8382  tz7.49  8384  oawordexr  8491  oewordi  8527  oeeulem  8537  nna0r  8545  nnawordex  8573  nnaordex  8574  nnaordex2  8575  oaabs  8584  oaabs2  8585  eldifsucnn  8600  elecex  8694  ectocld  8729  ecoptocl  8754  mapsnd  8834  eqeng  8933  difsnen  8997  fopwdom  9023  nneneq  9140  frfi  9195  elfiun  9343  ordiso  9431  ordtypelem7  9439  wemaplem2  9462  suc11reg  9540  inf3lem6  9554  noinfep  9581  cantnff  9595  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnflem1  9610  cantnf  9614  ttrcltr  9637  r111  9699  rankc2  9795  tcrank  9808  cardnueq0  9888  fodomfi2  9982  alephinit  10017  dfac9  10059  dfac12k  10070  djuinf  10111  ackbij1  10159  ackbij2  10164  sornom  10199  fin23lem16  10257  fin23lem21  10261  isf32lem2  10276  fin1a2lem6  10327  itunitc  10343  zorn2lem4  10421  wunr1om  10642  tskr1om  10690  recmulnq  10887  ltexnq  10898  distrlem4pr  10949  1re  11144  0re  11146  0cnALT  11381  0cnALT2  11382  mulge0  11668  prodgt0  12002  peano2nn  12186  recnz  12604  zneo  12612  uzn0  12805  xlemul1a  13240  prunioo  13434  flidz  13769  ceilidz  13811  modid2  13857  modmuladdnn0  13877  om2uzrani  13914  uzrdgfni  13920  seqid  14009  seqz  14012  facdiv  14249  facwordi  14251  hashdom  14341  wrdnval  14507  wrdnfi  14510  wrdl1s1  14577  sqrmo  15213  fsumf1o  15685  isumltss  15813  supcvg  15821  dvdsnegb  16242  dvdsexp2im  16296  odd2np1lem  16309  odd2np1  16310  ltoddhalfle  16330  halfleoddlt  16331  opoe  16332  omoe  16333  opeo  16334  omeo  16335  bitsuz  16443  bezoutlem4  16511  gcddiv  16520  gcdzeq  16521  dvdssqim  16523  dvdsexpim  16524  lcmgcdeq  16581  coprmdvds2  16623  rpmul  16628  divgcdcoprmex  16635  cncongr2  16637  dvdsprm  16673  coprm  16681  prmdvdsexp  16685  prmdiv  16755  pythagtriplem19  16804  pc2dvds  16850  pcadd  16860  prmpwdvds  16875  vdwlem11  16962  ramubcl  16989  0ram  16991  posasymb  18285  pleval2  18301  pltval3  18303  plttr  18306  pospo  18309  letsr  18559  intopsn  18622  ismgmid  18633  imasmnd2  18742  isgrpid2  18952  isgrpinv  18969  dfgrp3lem  19014  imasgrp2  19031  orbsta  19288  symgfix2  19391  pmtrfrn  19433  pmtrrn2  19435  odmulg  19531  odmulgeq  19532  gexdvdsi  19558  gexnnod  19563  pgpssslw  19589  sylow2alem1  19592  fislw  19600  lsmss1b  19641  lsmss2b  19643  efgrelexlemb  19725  torsubg  19829  ablfacrplem  20042  pgpfac1lem2  20052  pgpfac1lem3  20054  ablsimpnosubgd  20081  imasrng  20158  imasring  20310  dvdsrcl2  20346  dvdsrtr  20348  dvdsrmul1  20349  irredn0  20403  lspsneq0  21007  lmhmima  21042  lspsolv  21141  xrsdsreclblem  21393  dvdsrzring  21441  prmirredlem  21452  znunit  21543  pjdm2  21691  obselocv  21708  lindfrn  21801  opsrtoslem2  22034  mpfind  22093  psdmul  22132  mpfpf1  22316  pf1mpf  22317  cpmadugsumlemF  22841  baspartn  22919  bastop  22946  iscld3  23029  isopn3  23031  iscldtop  23060  ordtrest2lem  23168  2ndcredom  23415  2ndc1stc  23416  2ndcrest  23419  2ndcdisj  23421  2ndcsep  23424  kgenidm  23512  dfac14  23583  tx2ndc  23616  kqreglem1  23706  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  fmfnfm  23923  flimtopon  23935  fclstopon  23977  xrsmopn  24778  icccmplem2  24789  reconnlem1  24792  iccpnfcnv  24911  cphsqrtcl2  25153  ivthlem3  25420  ivthicc  25425  ovolctb  25457  ioombl  25532  itgabs  25802  itgsplitioo  25805  dvlip  25960  c1liplem1  25963  c1lip1  25964  dvgt0lem1  25969  dvivthlem2  25976  dvne0  25978  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  dvcvx  25987  itgsubstlem  26015  mdegnn0cl  26036  ig1peu  26140  elply2  26161  plypf1  26177  dgreq0  26230  aannenlem3  26296  abelthlem2  26397  lognegb  26554  eflogeq  26566  efopn  26622  cxpge0  26647  cxplea  26660  cxple2  26661  cxpcn3lem  26711  cxpaddlelem  26715  cxpaddle  26716  cxpeq  26721  asinsinb  26861  acoscosb  26862  atantanb  26888  wilthlem2  27032  sqf11  27102  sqff1o  27145  ppiublem1  27165  lgsdir  27295  lgsne0  27298  lgsquadlem3  27345  2sqblem  27394  dchrisum0flblem1  27471  ostth3  27601  ostth  27602  noseponlem  27628  nodenselem4  27651  nodenselem5  27652  nodenselem7  27654  nodenselem8  27655  nolt02o  27659  nogt01o  27660  nosupbnd2lem1  27679  noetasuplem4  27700  lesrec  27791  madebdayim  27880  negsproplem2  28021  negsunif  28047  negleft  28050  negright  28051  lemuls1ad  28174  precsexlem6  28204  precsexlem7  28205  noseqp1  28283  om2noseqlt  28291  noseqrdgfn  28298  bdayn0sf1o  28362  dfnns2  28364  bdayfinbndlem1  28459  colinearalg  28979  axcontlem5  29037  axcontlem9  29041  uhgrn0  29136  upgrfn  29156  umgrfn  29168  uvtxnbgrvtx  29462  vtxduhgr0nedg  29561  pthdivtx  29795  iswwlksnx  29908  wpthswwlks2on  30032  clwwlkn  30096  clwwlknonwwlknonb  30176  eupth2lem2  30289  eupth2lem3lem6  30303  htthlem  30988  pjpreeq  31469  h1dn0  31623  spansneleqi  31640  rnbra  32178  dfpjop  32253  elpjrn  32261  stm1i  32314  mdbr2  32367  mdsl2i  32393  sumdmdlem  32489  dmdbr6ati  32494  ordtrest2NEWlem  34066  xrge0iifcnv  34077  eulerpartlemb  34512  onvf1odlem4  35288  erdszelem8  35380  cvmlift3lem4  35504  cvmlift3lem5  35505  fmlasucdisj  35581  mrsub0  35698  mrsubccat  35700  mrsubcn  35701  msubrn  35711  msrid  35727  elmthm  35758  dfon2lem9  35971  btwnconn1lem11  36279  broutsideof2  36304  opnbnd  36507  tailfb  36559  tr0elw  36666  tr0el  36667  bj-ideqg1  37478  fin2so  37928  lindsadd  37934  poimirlem9  37950  poimirlem17  37958  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  itgabsnc  38010  ftc2nc  38023  sdclem2  38063  subspopn  38073  equivtotbnd  38099  rngosn3  38245  igenval2  38387  isfldidl  38389  relcnveq3  38648  iss2  38665  elrelscnveq3  38948  lshpinN  39435  lsatcv0eq  39493  lsatcv1  39494  cvrnbtwn3  39722  cvrnbtwn4  39725  cvrcmp  39729  atnlt  39759  cvlexchb1  39776  2llnne2N  39854  atcvr0eq  39872  lnnat  39873  cvrat4  39889  ps-1  39923  3at  39936  llncmp  39968  llnnlt  39969  llncvrlpln2  40003  llncvrlpln  40004  lplncmp  40008  lplnnlt  40011  lplncvrlvol2  40061  lplncvrlvol  40062  lvolcmp  40063  lvolnltN  40064  dalempnes  40097  dalemqnet  40098  dalem-cly  40117  dalem44  40162  lncmp  40229  cdlemblem  40239  llnexch2N  40316  osumcllem4N  40405  pexmidlem1N  40416  lhp2atnle  40479  cdleme11dN  40708  cdleme20k  40765  cdleme21at  40774  cdleme21ct  40775  cdleme32e  40891  cdleme35f  40900  tendoex  41421  dochexmidlem1  41906  lcfrlem9  41996  mapd1o  42094  mapdindp3  42168  zndvdchrrhm  42412  elre0re  42693  mullt0b2d  42929  flt0  43070  ismrc  43133  pellexlem1  43257  aomclem4  43485  dfac21  43494  lsmfgcl  43502  lmhmfgima  43512  dfacbasgrp  43536  hbtlem6  43557  fiuneneq  43620  oaabsb  43722  cantnfresb  43752  orbitcl  45384  stoweidlem27  46455  stoweidlem29  46457  fcoresf1  47517  tz6.12c-afv2  47690  dfatbrafv2b  47693  fnbrafv2b  47696  iccpartrn  47890  prmdvdsfmtnof1lem2  48048  mod42tp1mod8  48065  isubgredg  48342  grimuhgr  48363  grimcnv  48364  isuspgrim0  48370  assintopass  48690  rrxsphere  49224