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  3645  mob2  3673  rmob  3840  sneqrg  4795  preq1b  4802  prel12g  4820  disjxun  5096  sotric  5562  sotrieq  5563  iss  5994  poirr2  6081  xp11  6133  nordeq  6336  nsuceq0  6402  ordequn  6422  fnbrfvb  6884  2f1fvneq  7206  foeqcnvco  7246  f1eqcocnv  7247  dfwe2  7719  releldmdifi  7989  mposn  8045  poxp2  8085  poxp3  8092  poseq  8100  tfrlem15  8323  tz7.44-2  8338  tz7.48-1  8374  tz7.49  8376  oawordexr  8483  oewordi  8519  oeeulem  8529  nna0r  8537  nnawordex  8565  nnaordex  8566  nnaordex2  8567  oaabs  8576  oaabs2  8577  eldifsucnn  8592  elecex  8685  ectocld  8719  ecoptocl  8744  mapsnd  8824  eqeng  8923  difsnen  8987  fopwdom  9013  nneneq  9130  frfi  9185  elfiun  9333  ordiso  9421  ordtypelem7  9429  wemaplem2  9452  suc11reg  9528  inf3lem6  9542  noinfep  9569  cantnff  9583  cantnfp1lem2  9588  cantnfp1lem3  9589  cantnflem1  9598  cantnf  9602  ttrcltr  9625  r111  9687  rankc2  9783  tcrank  9796  cardnueq0  9876  fodomfi2  9970  alephinit  10005  dfac9  10047  dfac12k  10058  djuinf  10099  ackbij1  10147  ackbij2  10152  sornom  10187  fin23lem16  10245  fin23lem21  10249  isf32lem2  10264  fin1a2lem6  10315  itunitc  10331  zorn2lem4  10409  wunr1om  10630  tskr1om  10678  recmulnq  10875  ltexnq  10886  distrlem4pr  10937  1re  11132  0re  11134  0cnALT  11368  0cnALT2  11369  mulge0  11655  prodgt0  11988  peano2nn  12157  recnz  12567  zneo  12575  uzn0  12768  xlemul1a  13203  prunioo  13397  flidz  13730  ceilidz  13772  modid2  13818  modmuladdnn0  13838  om2uzrani  13875  uzrdgfni  13881  seqid  13970  seqz  13973  facdiv  14210  facwordi  14212  hashdom  14302  wrdnval  14468  wrdnfi  14471  wrdl1s1  14538  sqrmo  15174  fsumf1o  15646  isumltss  15771  supcvg  15779  dvdsnegb  16200  dvdsexp2im  16254  odd2np1lem  16267  odd2np1  16268  ltoddhalfle  16288  halfleoddlt  16289  opoe  16290  omoe  16291  opeo  16292  omeo  16293  bitsuz  16401  bezoutlem4  16469  gcddiv  16478  gcdzeq  16479  dvdssqim  16481  dvdsexpim  16482  lcmgcdeq  16539  coprmdvds2  16581  rpmul  16586  divgcdcoprmex  16593  cncongr2  16595  dvdsprm  16630  coprm  16638  prmdvdsexp  16642  prmdiv  16712  pythagtriplem19  16761  pc2dvds  16807  pcadd  16817  prmpwdvds  16832  vdwlem11  16919  ramubcl  16946  0ram  16948  posasymb  18242  pleval2  18258  pltval3  18260  plttr  18263  pospo  18266  letsr  18516  intopsn  18579  ismgmid  18590  imasmnd2  18699  isgrpid2  18906  isgrpinv  18923  dfgrp3lem  18968  imasgrp2  18985  orbsta  19242  symgfix2  19345  pmtrfrn  19387  pmtrrn2  19389  odmulg  19485  odmulgeq  19486  gexdvdsi  19512  gexnnod  19517  pgpssslw  19543  sylow2alem1  19546  fislw  19554  lsmss1b  19595  lsmss2b  19597  efgrelexlemb  19679  torsubg  19783  ablfacrplem  19996  pgpfac1lem2  20006  pgpfac1lem3  20008  ablsimpnosubgd  20035  imasrng  20112  imasring  20266  dvdsrcl2  20302  dvdsrtr  20304  dvdsrmul1  20305  irredn0  20359  lspsneq0  20963  lmhmima  20999  lspsolv  21098  xrsdsreclblem  21367  dvdsrzring  21416  prmirredlem  21427  znunit  21518  pjdm2  21666  obselocv  21683  lindfrn  21776  opsrtoslem2  22011  mpfind  22070  psdmul  22109  mpfpf1  22295  pf1mpf  22296  cpmadugsumlemF  22820  baspartn  22898  bastop  22925  iscld3  23008  isopn3  23010  iscldtop  23039  ordtrest2lem  23147  2ndcredom  23394  2ndc1stc  23395  2ndcrest  23398  2ndcdisj  23400  2ndcsep  23403  kgenidm  23491  dfac14  23562  tx2ndc  23595  kqreglem1  23685  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  fmfnfm  23902  flimtopon  23914  fclstopon  23956  xrsmopn  24757  icccmplem2  24768  reconnlem1  24771  iccpnfcnv  24898  cphsqrtcl2  25142  ivthlem3  25410  ivthicc  25415  ovolctb  25447  ioombl  25522  itgabs  25792  itgsplitioo  25795  dvlip  25954  c1liplem1  25957  c1lip1  25958  dvgt0lem1  25963  dvivthlem2  25970  dvne0  25972  lhop1lem  25974  lhop1  25975  lhop2  25976  lhop  25977  dvcvx  25981  itgsubstlem  26011  mdegnn0cl  26032  ig1peu  26136  elply2  26157  plypf1  26173  dgreq0  26227  aannenlem3  26294  abelthlem2  26398  lognegb  26555  eflogeq  26567  efopn  26623  cxpge0  26648  cxplea  26661  cxple2  26662  cxpcn3lem  26713  cxpaddlelem  26717  cxpaddle  26718  cxpeq  26723  asinsinb  26863  acoscosb  26864  atantanb  26890  wilthlem2  27035  sqf11  27105  sqff1o  27148  ppiublem1  27169  lgsdir  27299  lgsne0  27302  lgsquadlem3  27349  2sqblem  27398  dchrisum0flblem1  27475  ostth3  27605  ostth  27606  noseponlem  27632  nodenselem4  27655  nodenselem5  27656  nodenselem7  27658  nodenselem8  27659  nolt02o  27663  nogt01o  27664  nosupbnd2lem1  27683  noetasuplem4  27704  lesrec  27795  madebdayim  27884  negsproplem2  28025  negsunif  28051  negleft  28054  negright  28055  lemuls1ad  28178  precsexlem6  28208  precsexlem7  28209  noseqp1  28287  om2noseqlt  28295  noseqrdgfn  28302  bdayn0sf1o  28366  dfnns2  28368  bdayfinbndlem1  28463  colinearalg  28983  axcontlem5  29041  axcontlem9  29045  uhgrn0  29140  upgrfn  29160  umgrfn  29172  uvtxnbgrvtx  29466  vtxduhgr0nedg  29566  pthdivtx  29800  iswwlksnx  29913  wpthswwlks2on  30037  clwwlkn  30101  clwwlknonwwlknonb  30181  eupth2lem2  30294  eupth2lem3lem6  30308  htthlem  30992  pjpreeq  31473  h1dn0  31627  spansneleqi  31644  rnbra  32182  dfpjop  32257  elpjrn  32265  stm1i  32318  mdbr2  32371  mdsl2i  32397  sumdmdlem  32493  dmdbr6ati  32498  ordtrest2NEWlem  34079  xrge0iifcnv  34090  eulerpartlemb  34525  onvf1odlem4  35300  erdszelem8  35392  cvmlift3lem4  35516  cvmlift3lem5  35517  fmlasucdisj  35593  mrsub0  35710  mrsubccat  35712  mrsubcn  35713  msubrn  35723  msrid  35739  elmthm  35770  dfon2lem9  35983  btwnconn1lem11  36291  broutsideof2  36316  opnbnd  36519  tailfb  36571  bj-ideqg1  37369  fin2so  37808  lindsadd  37814  poimirlem9  37830  poimirlem17  37838  poimirlem26  37847  poimirlem27  37848  poimirlem31  37852  itgabsnc  37890  ftc2nc  37903  sdclem2  37943  subspopn  37953  equivtotbnd  37979  rngosn3  38125  igenval2  38267  isfldidl  38269  relcnveq3  38520  iss2  38537  elrelscnveq3  38800  lshpinN  39249  lsatcv0eq  39307  lsatcv1  39308  cvrnbtwn3  39536  cvrnbtwn4  39539  cvrcmp  39543  atnlt  39573  cvlexchb1  39590  2llnne2N  39668  atcvr0eq  39686  lnnat  39687  cvrat4  39703  ps-1  39737  3at  39750  llncmp  39782  llnnlt  39783  llncvrlpln2  39817  llncvrlpln  39818  lplncmp  39822  lplnnlt  39825  lplncvrlvol2  39875  lplncvrlvol  39876  lvolcmp  39877  lvolnltN  39878  dalempnes  39911  dalemqnet  39912  dalem-cly  39931  dalem44  39976  lncmp  40043  cdlemblem  40053  llnexch2N  40130  osumcllem4N  40219  pexmidlem1N  40230  lhp2atnle  40293  cdleme11dN  40522  cdleme20k  40579  cdleme21at  40588  cdleme21ct  40589  cdleme32e  40705  cdleme35f  40714  tendoex  41235  dochexmidlem1  41720  lcfrlem9  41810  mapd1o  41908  mapdindp3  41982  zndvdchrrhm  42226  elre0re  42509  mullt0b2d  42739  flt0  42880  ismrc  42943  pellexlem1  43071  aomclem4  43299  dfac21  43308  lsmfgcl  43316  lmhmfgima  43326  dfacbasgrp  43350  hbtlem6  43371  fiuneneq  43434  oaabsb  43536  cantnfresb  43566  orbitcl  45198  stoweidlem27  46271  stoweidlem29  46273  fcoresf1  47315  tz6.12c-afv2  47488  dfatbrafv2b  47491  fnbrafv2b  47494  iccpartrn  47676  prmdvdsfmtnof1lem2  47831  mod42tp1mod8  47848  isubgredg  48112  grimuhgr  48133  grimcnv  48134  isuspgrim0  48140  assintopass  48460  rrxsphere  48994