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  3675  mob2  3703  rmob  3870  sneqrg  4820  preq1b  4827  prel12g  4845  disjxun  5122  sotric  5596  sotrieq  5597  iss  6027  poirr2  6118  xp11  6169  nordeq  6376  nsuceq0  6442  ordequn  6462  tz6.12cOLD  6908  fnbrfvb  6934  2f1fvneq  7258  foeqcnvco  7298  f1eqcocnv  7299  dfwe2  7773  releldmdifi  8049  mposn  8107  poxp2  8147  poxp3  8154  poseq  8162  tfrlem15  8411  tz7.44-2  8426  tz7.48-1  8462  tz7.49  8464  oawordexr  8573  oewordi  8608  oeeulem  8618  nna0r  8626  nnawordex  8654  nnaordex  8655  nnaordex2  8656  oaabs  8665  oaabs2  8666  eldifsucnn  8681  ectocld  8803  ecoptocl  8826  mapsnd  8905  eqeng  9005  difsnen  9072  fopwdom  9099  nneneq  9225  frfi  9298  elfiun  9447  ordiso  9535  ordtypelem7  9543  wemaplem2  9566  suc11reg  9638  inf3lem6  9652  noinfep  9679  cantnff  9693  cantnfp1lem2  9698  cantnfp1lem3  9699  cantnflem1  9708  cantnf  9712  ttrcltr  9735  r111  9794  rankc2  9890  tcrank  9903  cardnueq0  9983  fodomfi2  10079  alephinit  10114  dfac9  10156  dfac12k  10167  djuinf  10208  ackbij1  10256  ackbij2  10261  sornom  10296  fin23lem16  10354  fin23lem21  10358  isf32lem2  10373  fin1a2lem6  10424  itunitc  10440  zorn2lem4  10518  wunr1om  10738  tskr1om  10786  recmulnq  10983  ltexnq  10994  distrlem4pr  11045  1re  11240  0re  11242  0cnALT  11475  0cnALT2  11476  mulge0  11760  prodgt0  12093  peano2nn  12257  recnz  12673  zneo  12681  uzn0  12874  xlemul1a  13309  prunioo  13503  flidz  13832  ceilidz  13874  modid2  13920  modmuladdnn0  13938  om2uzrani  13975  uzrdgfni  13981  seqid  14070  seqz  14073  facdiv  14310  facwordi  14312  hashdom  14402  wrdnval  14568  wrdnfi  14571  wrdl1s1  14637  sqrmo  15275  fsumf1o  15744  isumltss  15869  supcvg  15877  dvdsnegb  16298  dvdsexp2im  16351  odd2np1lem  16364  odd2np1  16365  ltoddhalfle  16385  halfleoddlt  16386  opoe  16387  omoe  16388  opeo  16389  omeo  16390  bitsuz  16498  bezoutlem4  16566  gcddiv  16575  gcdzeq  16576  dvdssqim  16578  dvdsexpim  16579  lcmgcdeq  16636  coprmdvds2  16678  rpmul  16683  divgcdcoprmex  16690  cncongr2  16692  dvdsprm  16727  coprm  16735  prmdvdsexp  16739  prmdiv  16809  pythagtriplem19  16858  pc2dvds  16904  pcadd  16914  prmpwdvds  16929  vdwlem11  17016  ramubcl  17043  0ram  17045  posasymb  18336  pleval2  18352  pltval3  18354  plttr  18357  pospo  18360  letsr  18608  intopsn  18637  ismgmid  18648  imasmnd2  18757  isgrpid2  18964  isgrpinv  18981  dfgrp3lem  19026  imasgrp2  19043  orbsta  19301  symgfix2  19402  pmtrfrn  19444  pmtrrn2  19446  odmulg  19542  odmulgeq  19543  gexdvdsi  19569  gexnnod  19574  pgpssslw  19600  sylow2alem1  19603  fislw  19611  lsmss1b  19652  lsmss2b  19654  efgrelexlemb  19736  torsubg  19840  ablfacrplem  20053  pgpfac1lem2  20063  pgpfac1lem3  20065  ablsimpnosubgd  20092  imasrng  20142  imasring  20295  dvdsrcl2  20331  dvdsrtr  20333  dvdsrmul1  20334  irredn0  20388  lspsneq0  20974  lmhmima  21010  lspsolv  21109  xrsdsreclblem  21385  dvdsrzring  21427  prmirredlem  21438  znunit  21529  pjdm2  21676  obselocv  21693  lindfrn  21786  opsrtoslem2  22019  mpfind  22070  psdmul  22109  mpfpf1  22294  pf1mpf  22295  cpmadugsumlemF  22819  baspartn  22897  bastop  22924  iscld3  23007  isopn3  23009  iscldtop  23038  ordtrest2lem  23146  2ndcredom  23393  2ndc1stc  23394  2ndcrest  23397  2ndcdisj  23399  2ndcsep  23402  kgenidm  23490  dfac14  23561  tx2ndc  23594  kqreglem1  23684  rnelfm  23896  fmfnfmlem2  23898  fmfnfmlem4  23900  fmfnfm  23901  flimtopon  23913  fclstopon  23955  xrsmopn  24757  icccmplem2  24768  reconnlem1  24771  iccpnfcnv  24898  cphsqrtcl2  25143  ivthlem3  25411  ivthicc  25416  ovolctb  25448  ioombl  25523  itgabs  25793  itgsplitioo  25796  dvlip  25955  c1liplem1  25958  c1lip1  25959  dvgt0lem1  25964  dvivthlem2  25971  dvne0  25973  lhop1lem  25975  lhop1  25976  lhop2  25977  lhop  25978  dvcvx  25982  itgsubstlem  26012  mdegnn0cl  26033  ig1peu  26137  elply2  26158  plypf1  26174  dgreq0  26228  aannenlem3  26295  abelthlem2  26399  lognegb  26556  eflogeq  26568  efopn  26624  cxpge0  26649  cxplea  26662  cxple2  26663  cxpcn3lem  26714  cxpaddlelem  26718  cxpaddle  26719  cxpeq  26724  asinsinb  26864  acoscosb  26865  atantanb  26891  wilthlem2  27036  sqf11  27106  sqff1o  27149  ppiublem1  27170  lgsdir  27300  lgsne0  27303  lgsquadlem3  27350  2sqblem  27399  dchrisum0flblem1  27476  ostth3  27606  ostth  27607  noseponlem  27633  nodenselem4  27656  nodenselem5  27657  nodenselem7  27659  nodenselem8  27660  nolt02o  27664  nogt01o  27665  nosupbnd2lem1  27684  noetasuplem4  27705  slerec  27788  madebdayim  27856  negsproplem2  27992  negsunif  28018  slemul1ad  28142  precsexlem6  28171  precsexlem7  28172  noseqp1  28242  om2noseqlt  28250  noseqrdgfn  28257  bdayn0sf1o  28316  dfnns2  28318  colinearalg  28894  axcontlem5  28952  axcontlem9  28956  uhgrn0  29051  upgrfn  29071  umgrfn  29083  uvtxnbgrvtx  29377  vtxduhgr0nedg  29477  pthdivtx  29714  iswwlksnx  29827  wpthswwlks2on  29948  clwwlkn  30012  clwwlknonwwlknonb  30092  eupth2lem2  30205  eupth2lem3lem6  30219  htthlem  30903  pjpreeq  31384  h1dn0  31538  spansneleqi  31555  rnbra  32093  dfpjop  32168  elpjrn  32176  stm1i  32229  mdbr2  32282  mdsl2i  32308  sumdmdlem  32404  dmdbr6ati  32409  ordtrest2NEWlem  33958  xrge0iifcnv  33969  eulerpartlemb  34405  erdszelem8  35225  cvmlift3lem4  35349  cvmlift3lem5  35350  fmlasucdisj  35426  mrsub0  35543  mrsubccat  35545  mrsubcn  35546  msubrn  35556  msrid  35572  elmthm  35603  dfon2lem9  35814  btwnconn1lem11  36120  broutsideof2  36145  opnbnd  36348  tailfb  36400  bj-ideqg1  37187  fin2so  37636  lindsadd  37642  poimirlem9  37658  poimirlem17  37666  poimirlem26  37675  poimirlem27  37676  poimirlem31  37680  itgabsnc  37718  ftc2nc  37731  sdclem2  37771  subspopn  37781  equivtotbnd  37807  rngosn3  37953  igenval2  38095  isfldidl  38097  relcnveq3  38344  ecex2  38351  iss2  38367  elrelscnveq3  38514  lshpinN  39012  lsatcv0eq  39070  lsatcv1  39071  cvrnbtwn3  39299  cvrnbtwn4  39302  cvrcmp  39306  atnlt  39336  cvlexchb1  39353  2llnne2N  39432  atcvr0eq  39450  lnnat  39451  cvrat4  39467  ps-1  39501  3at  39514  llncmp  39546  llnnlt  39547  llncvrlpln2  39581  llncvrlpln  39582  lplncmp  39586  lplnnlt  39589  lplncvrlvol2  39639  lplncvrlvol  39640  lvolcmp  39641  lvolnltN  39642  dalempnes  39675  dalemqnet  39676  dalem-cly  39695  dalem44  39740  lncmp  39807  cdlemblem  39817  llnexch2N  39894  osumcllem4N  39983  pexmidlem1N  39994  lhp2atnle  40057  cdleme11dN  40286  cdleme20k  40343  cdleme21at  40352  cdleme21ct  40353  cdleme32e  40469  cdleme35f  40478  tendoex  40999  dochexmidlem1  41484  lcfrlem9  41574  mapd1o  41672  mapdindp3  41746  zndvdchrrhm  41990  elre0re  42272  flt0  42635  ismrc  42699  pellexlem1  42827  aomclem4  43056  dfac21  43065  lsmfgcl  43073  lmhmfgima  43083  dfacbasgrp  43107  hbtlem6  43128  fiuneneq  43191  oaabsb  43293  cantnfresb  43323  orbitcl  44957  stoweidlem27  46036  stoweidlem29  46038  fcoresf1  47078  tz6.12c-afv2  47251  dfatbrafv2b  47254  fnbrafv2b  47257  iccpartrn  47424  prmdvdsfmtnof1lem2  47579  mod42tp1mod8  47596  isubgredg  47859  grimuhgr  47880  grimcnv  47881  isuspgrim0  47887  assintopass  48169  rrxsphere  48708