Theorem syl5ibcom 244

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

Ref	Expression
syl5ib.1	⊢ (𝜑 → 𝜓)
syl5ib.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibcom	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5ib.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5ib 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  3624  mob2  3651  rmob  3824  sneqrg  4771  preq1b  4778  prel12g  4795  disjxun  5073  sotric  5532  sotrieq  5533  iss  5946  poirr2  6034  xp11  6083  nordeq  6289  nsuceq0  6350  ordequn  6370  tz6.12c  6808  fnbrfvb  6831  foeqcnvco  7181  f1eqcocnv  7182  f1eqcocnvOLD  7183  dfwe2  7633  releldmdifi  7895  mposn  7952  tfrlem15  8232  tz7.44-2  8247  tz7.48-1  8283  tz7.49  8285  oawordexr  8396  oewordi  8431  oeeulem  8441  nna0r  8449  nnawordex  8477  nnaordex  8478  oaabs  8487  oaabs2  8488  eldifsucnn  8503  ectocld  8582  ecoptocl  8605  mapsnd  8683  eqeng  8783  difsnen  8849  fopwdom  8876  nneneq  9001  frfi  9068  elfiun  9198  ordiso  9284  ordtypelem7  9292  wemaplem2  9315  suc11reg  9386  inf3lem6  9400  noinfep  9427  cantnff  9441  cantnfp1lem2  9446  cantnfp1lem3  9447  cantnflem1  9456  cantnf  9460  ttrcltr  9483  r111  9542  rankc2  9638  tcrank  9651  cardnueq0  9731  fodomfi2  9825  alephinit  9860  dfac9  9901  dfac12k  9912  djuinf  9953  ackbij1  10003  ackbij2  10008  sornom  10042  fin23lem16  10100  fin23lem21  10104  isf32lem2  10119  fin1a2lem6  10170  itunitc  10186  zorn2lem4  10264  wunr1om  10484  tskr1om  10532  recmulnq  10729  ltexnq  10740  distrlem4pr  10791  1re  10984  0re  10986  0cnALT  11218  0cnALT2  11219  mulge0  11502  prodgt0  11831  peano2nn  11994  recnz  12404  zneo  12412  uzn0  12608  xlemul1a  13031  prunioo  13222  flidz  13539  ceilidz  13581  modid2  13627  modmuladdnn0  13644  om2uzrani  13681  uzrdgfni  13687  seqid  13777  seqz  13780  facdiv  14010  facwordi  14012  hashdom  14103  wrdnval  14257  wrdnfi  14260  wrdl1s1  14328  sqrmo  14972  fsumf1o  15444  isumltss  15569  supcvg  15577  dvdsnegb  15992  dvdsexp2im  16045  odd2np1lem  16058  odd2np1  16059  ltoddhalfle  16079  halfleoddlt  16080  opoe  16081  omoe  16082  opeo  16083  omeo  16084  bitsuz  16190  bezoutlem4  16259  gcddiv  16268  gcdzeq  16271  dvdssqim  16273  lcmgcdeq  16326  coprmdvds2  16368  rpmul  16373  divgcdcoprmex  16380  cncongr2  16382  dvdsprm  16417  coprm  16425  prmdvdsexp  16429  prmdiv  16495  pythagtriplem19  16543  pc2dvds  16589  pcadd  16599  prmpwdvds  16614  vdwlem11  16701  ramubcl  16728  0ram  16730  posasymb  18046  pleval2  18064  pltval3  18066  plttr  18069  pospo  18072  letsr  18320  intopsn  18347  ismgmid  18358  imasmnd2  18431  isgrpid2  18625  isgrpinv  18641  dfgrp3lem  18682  imasgrp2  18699  orbsta  18928  symgfix2  19033  pmtrfrn  19075  pmtrrn2  19077  odmulg  19172  odmulgeq  19173  gexdvdsi  19197  gexnnod  19202  pgpssslw  19228  sylow2alem1  19231  fislw  19239  lsmss1b  19281  lsmss2b  19283  efgrelexlemb  19365  torsubg  19464  ablfacrplem  19677  pgpfac1lem2  19687  pgpfac1lem3  19689  ablsimpnosubgd  19716  imasring  19867  dvdsrcl2  19901  dvdsrtr  19903  dvdsrmul1  19904  irredn0  19954  lspsneq0  20283  lmhmima  20318  lspsolv  20414  xrsdsreclblem  20653  dvdsrzring  20692  prmirredlem  20703  znunit  20780  pjdm2  20927  obselocv  20944  lindfrn  21037  opsrtoslem2  21272  mpfind  21326  mpfpf1  21526  pf1mpf  21527  cpmadugsumlemF  22034  baspartn  22113  bastop  22140  iscld3  22224  isopn3  22226  iscldtop  22255  ordtrest2lem  22363  2ndcredom  22610  2ndc1stc  22611  2ndcrest  22614  2ndcdisj  22616  2ndcsep  22619  kgenidm  22707  dfac14  22778  tx2ndc  22811  kqreglem1  22901  rnelfm  23113  fmfnfmlem2  23115  fmfnfmlem4  23117  fmfnfm  23118  flimtopon  23130  fclstopon  23172  xrsmopn  23984  icccmplem2  23995  reconnlem1  23998  iccpnfcnv  24116  cphsqrtcl2  24359  ivthlem3  24626  ivthicc  24631  ovolctb  24663  ioombl  24738  itgabs  25008  itgsplitioo  25011  dvlip  25166  c1liplem1  25169  c1lip1  25170  dvgt0lem1  25175  dvivthlem2  25182  dvne0  25184  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  dvcvx  25193  itgsubstlem  25221  mdegnn0cl  25245  ig1peu  25345  elply2  25366  plypf1  25382  dgreq0  25435  aannenlem3  25499  abelthlem2  25600  lognegb  25754  eflogeq  25766  efopn  25822  cxpge0  25847  cxplea  25860  cxple2  25861  cxpcn3lem  25909  cxpaddlelem  25913  cxpaddle  25914  cxpeq  25919  asinsinb  26056  acoscosb  26057  atantanb  26083  wilthlem2  26227  sqf11  26297  sqff1o  26340  ppiublem1  26359  lgsdir  26489  lgsne0  26492  lgsquadlem3  26539  2sqblem  26588  dchrisum0flblem1  26665  ostth3  26795  ostth  26796  colinearalg  27287  axcontlem5  27345  axcontlem9  27349  uhgrn0  27446  upgrfn  27466  umgrfn  27478  uvtxnbgrvtx  27769  vtxduhgr0nedg  27868  pthdivtx  28106  iswwlksnx  28214  wpthswwlks2on  28335  clwwlkn  28399  clwwlknonwwlknonb  28479  eupth2lem2  28592  eupth2lem3lem6  28606  htthlem  29288  pjpreeq  29769  h1dn0  29923  spansneleqi  29940  rnbra  30478  dfpjop  30553  elpjrn  30561  stm1i  30614  mdbr2  30667  mdsl2i  30693  sumdmdlem  30789  dmdbr6ati  30794  ordtrest2NEWlem  31881  xrge0iifcnv  31892  eulerpartlemb  32344  erdszelem8  33169  cvmlift3lem4  33293  cvmlift3lem5  33294  fmlasucdisj  33370  mrsub0  33487  mrsubccat  33489  mrsubcn  33490  msubrn  33500  msrid  33516  elmthm  33547  dfon2lem9  33776  poxp2  33799  poxp3  33805  poseq  33811  noseponlem  33876  nodenselem4  33899  nodenselem5  33900  nodenselem7  33902  nodenselem8  33903  nolt02o  33907  nogt01o  33908  nosupbnd2lem1  33927  noetasuplem4  33948  slerec  34022  madebdayim  34079  btwnconn1lem11  34408  broutsideof2  34433  opnbnd  34523  tailfb  34575  bj-ideqg1  35344  fin2so  35773  lindsadd  35779  poimirlem9  35795  poimirlem17  35803  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  itgabsnc  35855  ftc2nc  35868  sdclem2  35909  subspopn  35919  equivtotbnd  35945  rngosn3  36091  igenval2  36233  isfldidl  36235  relcnveq3  36463  ecex2  36470  iss2  36486  elrelscnveq3  36616  lshpinN  37010  lsatcv0eq  37068  lsatcv1  37069  cvrnbtwn3  37297  cvrnbtwn4  37300  cvrcmp  37304  atnlt  37334  cvlexchb1  37351  2llnne2N  37429  atcvr0eq  37447  lnnat  37448  cvrat4  37464  ps-1  37498  3at  37511  llncmp  37543  llnnlt  37544  llncvrlpln2  37578  llncvrlpln  37579  lplncmp  37583  lplnnlt  37586  lplncvrlvol2  37636  lplncvrlvol  37637  lvolcmp  37638  lvolnltN  37639  dalempnes  37672  dalemqnet  37673  dalem-cly  37692  dalem44  37737  lncmp  37804  cdlemblem  37814  llnexch2N  37891  osumcllem4N  37980  pexmidlem1N  37991  lhp2atnle  38054  cdleme11dN  38283  cdleme20k  38340  cdleme21at  38349  cdleme21ct  38350  cdleme32e  38466  cdleme35f  38475  tendoex  38996  dochexmidlem1  39481  lcfrlem9  39571  mapd1o  39669  mapdindp3  39743  elre0re  40298  dvdsexpim  40335  flt0  40481  ismrc  40530  pellexlem1  40658  aomclem4  40889  dfac21  40898  lsmfgcl  40906  lmhmfgima  40916  dfacbasgrp  40940  hbtlem6  40961  fiuneneq  41029  stoweidlem27  43575  stoweidlem29  43577  fcoresf1  44574  tz6.12c-afv2  44745  dfatbrafv2b  44748  fnbrafv2b  44751  iccpartrn  44893  prmdvdsfmtnof1lem2  45048  mod42tp1mod8  45065  assintopass  45419  rrxsphere  46105