Theorem syl5ibcom 244

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimpcd  248  elrab3t  3681  mob2  3710  rmob  3883  sneqrg  4839  preq1b  4846  prel12g  4863  disjxun  5145  sotric  5615  sotrieq  5616  iss  6033  poirr2  6122  xp11  6171  nordeq  6380  nsuceq0  6444  ordequn  6464  tz6.12cOLD  6915  fnbrfvb  6941  foeqcnvco  7294  f1eqcocnv  7295  f1eqcocnvOLD  7296  dfwe2  7757  releldmdifi  8027  mposn  8085  poxp2  8125  poxp3  8132  poseq  8140  tfrlem15  8388  tz7.44-2  8403  tz7.48-1  8439  tz7.49  8441  oawordexr  8552  oewordi  8587  oeeulem  8597  nna0r  8605  nnawordex  8633  nnaordex  8634  oaabs  8643  oaabs2  8644  eldifsucnn  8659  ectocld  8774  ecoptocl  8797  mapsnd  8876  eqeng  8978  difsnen  9049  fopwdom  9076  nneneq  9205  frfi  9284  elfiun  9421  ordiso  9507  ordtypelem7  9515  wemaplem2  9538  suc11reg  9610  inf3lem6  9624  noinfep  9651  cantnff  9665  cantnfp1lem2  9670  cantnfp1lem3  9671  cantnflem1  9680  cantnf  9684  ttrcltr  9707  r111  9766  rankc2  9862  tcrank  9875  cardnueq0  9955  fodomfi2  10051  alephinit  10086  dfac9  10127  dfac12k  10138  djuinf  10179  ackbij1  10229  ackbij2  10234  sornom  10268  fin23lem16  10326  fin23lem21  10330  isf32lem2  10345  fin1a2lem6  10396  itunitc  10412  zorn2lem4  10490  wunr1om  10710  tskr1om  10758  recmulnq  10955  ltexnq  10966  distrlem4pr  11017  1re  11210  0re  11212  0cnALT  11444  0cnALT2  11445  mulge0  11728  prodgt0  12057  peano2nn  12220  recnz  12633  zneo  12641  uzn0  12835  xlemul1a  13263  prunioo  13454  flidz  13771  ceilidz  13813  modid2  13859  modmuladdnn0  13876  om2uzrani  13913  uzrdgfni  13919  seqid  14009  seqz  14012  facdiv  14243  facwordi  14245  hashdom  14335  wrdnval  14491  wrdnfi  14494  wrdl1s1  14560  sqrmo  15194  fsumf1o  15665  isumltss  15790  supcvg  15798  dvdsnegb  16213  dvdsexp2im  16266  odd2np1lem  16279  odd2np1  16280  ltoddhalfle  16300  halfleoddlt  16301  opoe  16302  omoe  16303  opeo  16304  omeo  16305  bitsuz  16411  bezoutlem4  16480  gcddiv  16489  gcdzeq  16490  dvdssqim  16492  lcmgcdeq  16545  coprmdvds2  16587  rpmul  16592  divgcdcoprmex  16599  cncongr2  16601  dvdsprm  16636  coprm  16644  prmdvdsexp  16648  prmdiv  16714  pythagtriplem19  16762  pc2dvds  16808  pcadd  16818  prmpwdvds  16833  vdwlem11  16920  ramubcl  16947  0ram  16949  posasymb  18268  pleval2  18286  pltval3  18288  plttr  18291  pospo  18294  letsr  18542  intopsn  18569  ismgmid  18580  imasmnd2  18658  isgrpid2  18857  isgrpinv  18874  dfgrp3lem  18917  imasgrp2  18934  orbsta  19171  symgfix2  19278  pmtrfrn  19320  pmtrrn2  19322  odmulg  19418  odmulgeq  19419  gexdvdsi  19445  gexnnod  19450  pgpssslw  19476  sylow2alem1  19479  fislw  19487  lsmss1b  19528  lsmss2b  19530  efgrelexlemb  19612  torsubg  19716  ablfacrplem  19929  pgpfac1lem2  19939  pgpfac1lem3  19941  ablsimpnosubgd  19968  imasring  20136  dvdsrcl2  20172  dvdsrtr  20174  dvdsrmul1  20175  irredn0  20229  lspsneq0  20615  lmhmima  20650  lspsolv  20748  xrsdsreclblem  20983  dvdsrzring  21022  prmirredlem  21033  znunit  21110  pjdm2  21257  obselocv  21274  lindfrn  21367  opsrtoslem2  21608  mpfind  21661  mpfpf1  21861  pf1mpf  21862  cpmadugsumlemF  22369  baspartn  22448  bastop  22475  iscld3  22559  isopn3  22561  iscldtop  22590  ordtrest2lem  22698  2ndcredom  22945  2ndc1stc  22946  2ndcrest  22949  2ndcdisj  22951  2ndcsep  22954  kgenidm  23042  dfac14  23113  tx2ndc  23146  kqreglem1  23236  rnelfm  23448  fmfnfmlem2  23450  fmfnfmlem4  23452  fmfnfm  23453  flimtopon  23465  fclstopon  23507  xrsmopn  24319  icccmplem2  24330  reconnlem1  24333  iccpnfcnv  24451  cphsqrtcl2  24694  ivthlem3  24961  ivthicc  24966  ovolctb  24998  ioombl  25073  itgabs  25343  itgsplitioo  25346  dvlip  25501  c1liplem1  25504  c1lip1  25505  dvgt0lem1  25510  dvivthlem2  25517  dvne0  25519  lhop1lem  25521  lhop1  25522  lhop2  25523  lhop  25524  dvcvx  25528  itgsubstlem  25556  mdegnn0cl  25580  ig1peu  25680  elply2  25701  plypf1  25717  dgreq0  25770  aannenlem3  25834  abelthlem2  25935  lognegb  26089  eflogeq  26101  efopn  26157  cxpge0  26182  cxplea  26195  cxple2  26196  cxpcn3lem  26244  cxpaddlelem  26248  cxpaddle  26249  cxpeq  26254  asinsinb  26391  acoscosb  26392  atantanb  26418  wilthlem2  26562  sqf11  26632  sqff1o  26675  ppiublem1  26694  lgsdir  26824  lgsne0  26827  lgsquadlem3  26874  2sqblem  26923  dchrisum0flblem1  27000  ostth3  27130  ostth  27131  noseponlem  27156  nodenselem4  27179  nodenselem5  27180  nodenselem7  27182  nodenselem8  27183  nolt02o  27187  nogt01o  27188  nosupbnd2lem1  27207  noetasuplem4  27228  slerec  27309  madebdayim  27371  negsproplem2  27492  negsunif  27518  precsexlem6  27647  precsexlem7  27648  colinearalg  28157  axcontlem5  28215  axcontlem9  28219  uhgrn0  28316  upgrfn  28336  umgrfn  28348  uvtxnbgrvtx  28639  vtxduhgr0nedg  28738  pthdivtx  28975  iswwlksnx  29083  wpthswwlks2on  29204  clwwlkn  29268  clwwlknonwwlknonb  29348  eupth2lem2  29461  eupth2lem3lem6  29475  htthlem  30157  pjpreeq  30638  h1dn0  30792  spansneleqi  30809  rnbra  31347  dfpjop  31422  elpjrn  31430  stm1i  31483  mdbr2  31536  mdsl2i  31562  sumdmdlem  31658  dmdbr6ati  31663  ordtrest2NEWlem  32890  xrge0iifcnv  32901  eulerpartlemb  33355  erdszelem8  34177  cvmlift3lem4  34301  cvmlift3lem5  34302  fmlasucdisj  34378  mrsub0  34495  mrsubccat  34497  mrsubcn  34498  msubrn  34508  msrid  34524  elmthm  34555  dfon2lem9  34751  btwnconn1lem11  35057  broutsideof2  35082  opnbnd  35198  tailfb  35250  bj-ideqg1  36033  fin2so  36463  lindsadd  36469  poimirlem9  36485  poimirlem17  36493  poimirlem26  36502  poimirlem27  36503  poimirlem31  36507  itgabsnc  36545  ftc2nc  36558  sdclem2  36598  subspopn  36608  equivtotbnd  36634  rngosn3  36780  igenval2  36922  isfldidl  36924  relcnveq3  37178  ecex2  37185  iss2  37201  elrelscnveq3  37349  lshpinN  37847  lsatcv0eq  37905  lsatcv1  37906  cvrnbtwn3  38134  cvrnbtwn4  38137  cvrcmp  38141  atnlt  38171  cvlexchb1  38188  2llnne2N  38267  atcvr0eq  38285  lnnat  38286  cvrat4  38302  ps-1  38336  3at  38349  llncmp  38381  llnnlt  38382  llncvrlpln2  38416  llncvrlpln  38417  lplncmp  38421  lplnnlt  38424  lplncvrlvol2  38474  lplncvrlvol  38475  lvolcmp  38476  lvolnltN  38477  dalempnes  38510  dalemqnet  38511  dalem-cly  38530  dalem44  38575  lncmp  38642  cdlemblem  38652  llnexch2N  38729  osumcllem4N  38818  pexmidlem1N  38829  lhp2atnle  38892  cdleme11dN  39121  cdleme20k  39178  cdleme21at  39187  cdleme21ct  39188  cdleme32e  39304  cdleme35f  39313  tendoex  39834  dochexmidlem1  40319  lcfrlem9  40409  mapd1o  40507  mapdindp3  40581  elre0re  41172  dvdsexpim  41214  flt0  41375  ismrc  41424  pellexlem1  41552  aomclem4  41784  dfac21  41793  lsmfgcl  41801  lmhmfgima  41811  dfacbasgrp  41835  hbtlem6  41856  fiuneneq  41924  oaabsb  42029  cantnfresb  42059  stoweidlem27  44729  stoweidlem29  44731  fcoresf1  45765  tz6.12c-afv2  45936  dfatbrafv2b  45939  fnbrafv2b  45942  iccpartrn  46084  prmdvdsfmtnof1lem2  46239  mod42tp1mod8  46256  assintopass  46610  imasrng  46664  rrxsphere  47387