Theorem sylibd 242

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

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

Assertion

Ref	Expression
sylibd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	2	biimpd 232	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3d  296  ceqsalt  3428  sbceqal  3749  csbiebt  3828  rspcsbela  4336  sneqrg  4736  preq1b  4743  csbexg  5188  elrnrexdm  6886  isoselem  7128  riotass2  7179  ordzsl  7602  oaword2  8259  oaordex  8264  omword1  8279  om00  8281  omeulem2  8289  oen0  8292  oeeui  8308  nnaordex  8344  php3  8810  onomeneq  8845  frfi  8894  infglb  9084  suc11reg  9212  cardne  9546  cardsdomel  9555  carduni  9562  acndom  9630  alephinit  9674  cfflb  9838  cfslb2n  9847  fin23lem28  9919  isf34lem6  9959  fin1a2lem9  9987  axcc3  10017  winalim2  10275  inar1  10354  rankcf  10356  addclprlem2  10596  mulclprlem  10598  ltexprlem7  10621  prlem936  10626  reclem4pr  10629  sqgt0sr  10685  ltord2  11326  leord2  11327  eqord2  11328  mulgt1  11656  mulge0b  11667  lt2halves  12030  addltmul  12031  ltsubnn0  12106  nzadd  12190  zextlt  12216  recnz  12217  zeo  12228  peano5uzi  12231  uzm1  12437  irradd  12534  irrmul  12535  xltneg  12772  xleadd1  12810  xmulasslem  12840  xlemul1a  12843  xlemul1  12845  fznuz  13159  uznfz  13160  axdc4uzlem  13521  facndiv  13819  hashvnfin  13892  hashgt12el  13954  hashgt12el2  13955  hashf1  13988  ccatalpha  14115  swrdccatin2  14259  swrdccatin2d  14274  rennim  14767  cau3lem  14883  caubnd2  14886  o1lo1  15063  climrlim2  15073  climshft  15102  subcn2  15121  mulcn2  15122  rlimo1  15143  o1dif  15156  isercoll  15196  caucvgrlem  15201  serf0  15209  cvgrat  15410  efieq1re  15723  moddvds  15789  dvdsssfz1  15842  smuval2  16004  nn0seqcvgd  16090  algcvgblem  16097  eucalglt  16105  lcmgcdlem  16126  rpmul  16179  divgcdcoprm0  16185  isprm6  16234  rpexp  16242  eulerthlem2  16298  prmdiv  16301  pcprendvds2  16357  pcz  16397  pcprmpw  16399  pcadd2  16406  pcfac  16415  expnprm  16418  ramlb  16535  firest  16891  joineu  17842  meeteu  17856  latjlej1  17913  latjlej2  17914  latmlem1  17929  latmlem2  17930  lubun  17975  acsmapd  18014  imasgrp2  18432  issubg4  18516  psgnunilem4  18843  oddvdsnn0  18890  odmulgeq  18902  subgpgp  18940  odcau  18947  lsmlub  19008  frgpnabllem1  19212  pgpfac1lem2  19416  pgpfac1lem3a  19417  pgpfac1lem3  19418  irredrmul  19679  islmhm2  20029  lsmelval2  20076  lspsnat  20136  znidomb  20480  ip2eq  20569  lsmcss  20608  cnpnei  22115  cncls2  22124  cncls  22125  cnntr  22126  cnt0  22197  isnrm2  22209  comppfsc  22383  kqcldsat  22584  isr0  22588  hmeoopn  22617  hmeocld  22618  trufil  22761  opnsubg  22959  ghmcnp  22966  tgphaus  22968  qustgpopn  22971  tsmsgsum  22990  isngp4  23464  xrhmeo  23797  bndth  23809  cfilres  24147  caubl  24159  ivthlem2  24303  ovolicc2  24373  ismbf3d  24505  itg1ge0a  24563  mbfi1flim  24575  itg2gt0  24612  dvge0  24857  dvcnvrelem1  24868  dvcvx  24871  mdegmullem  24930  ig1peu  25023  plyco  25089  coemulc  25103  dgreq0  25113  dgrlt  25114  plymul0or  25128  plydiveu  25145  quotcan  25156  aalioulem3  25181  ulmcaulem  25240  sincosq3sgn  25344  sincosq4sgn  25345  sineq0  25367  logrec  25600  xrlimcnp  25805  cxploglim  25814  lgamgulmlem1  25865  mumul  26017  chtub  26047  perfect1  26063  dchrelbas3  26073  lgsdir2lem4  26163  lgsne0  26170  lgsquad2lem2  26220  2sqlem8a  26260  2sqblem  26266  axcontlem2  27010  elntg2  27030  redwlklem  27713  redwlk  27714  crctcshwlkn0lem3  27850  crctcshwlkn0lem5  27852  clwwlkext2edg  28093  wwlksubclwwlk  28095  frgrwopregasn  28353  frgrwopregbsn  28354  blocnilem  28839  ip2eqi  28891  ubthlem2  28906  hial0  29137  hial02  29138  hial2eq  29141  h1datomi  29616  sumspansn  29684  lnopcnbd  30071  riesz4i  30098  bra11  30143  pjss2coi  30199  pjnormssi  30203  pjorthcoi  30204  pjclem4a  30233  pj3lem1  30241  pj3cor1i  30244  hst1h  30262  stm1i  30278  strlem1  30285  golem2  30307  mdbr2  30331  dmdbr5  30343  mdsl2i  30357  atexch  30416  atcvatlem  30420  chirredlem1  30425  cdjreui  30467  cdj1i  30468  cdj3lem1  30469  xraddge02  30753  submarchi  31113  isarchiofld  31189  esumcvg  31720  bnj1468  32493  loop1cycl  32766  erdsze2lem2  32833  funeldmb  33407  nogt01o  33585  sltlpss  33773  btwnexch  34013  btwncolinear2  34058  btwncolinear3  34059  btwncolinear4  34060  btwncolinear5  34061  btwncolinear6  34062  nn0prpw  34198  cldbnd  34201  onsuct0  34316  onint1  34324  bj-ceqsalt0  34756  bj-ceqsalt1  34757  bj-inftyexpiinj  35064  bj-bary1lem1  35165  bj-bary1  35166  relowlssretop  35220  isinf2  35262  ltflcei  35451  tan2h  35455  poimirlem26  35489  poimirlem31  35494  ftc1anclem6  35541  dvasin  35547  dvacos  35548  fdc  35589  caushft  35605  heibor1lem  35653  bfplem2  35667  rrncmslem  35676  rngosn3  35768  mpobi123f  36006  riotasv3d  36660  lsatcv1  36748  lub0N  36889  glb0N  36893  oplecon3b  36900  cmtbr4N  36955  cvrnbtwn2  36975  atnlt  37013  atlatle  37020  cvlsupr2  37043  cvrexchlem  37119  cvratlem  37121  atcvrj0  37128  cvrat4  37143  cvrat42  37144  4noncolr3  37153  ps-1  37177  llnnlt  37223  lplnnlt  37265  lvolnltN  37318  dalempnes  37351  dalemqnet  37352  dalem-cly  37371  dalem44  37416  pmaple  37461  cdlemblem  37493  paddss  37545  2polcon4bN  37618  ltrneq2  37848  cdlemc3  37893  cdleme11h  37966  cdleme16b  37979  cdlemednpq  37999  tendospcanN  38723  dihmeetlem13N  39019  mapdordlem2  39337  mapdn0  39369  isdomn4  39835  ccatcan2d  39873  ctbnfien  40284  rmxypairf1o  40377  monotoddzzfi  40408  oddcomabszz  40410  acongtr  40444  frege124d  40987  expgrowth  41567  sbcbi  41773  limsupmnflem  42879  funressnfv  44152  funfocofob  44185  2elfz2melfz  44426  iccpartnel  44506  requad2  44691  uzlidlring  45103  ply1mulgsumlem2  45344  fllog2  45530  dignn0flhalflem1  45577