Theorem sylibd 149

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 144	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3d  202  dvelimdf  2076  ceqsalt  2848  sbceqal  3107  csbiebt  3187  rspcsbela  3207  preqr1g  3891  repizf2  4301  copsexg  4386  onun2  4639  suc11g  4706  elrnrexdm  5850  isoselem  6029  riotass2  6070  oawordriexmid  6747  nnm00  6807  ecopovtrn  6910  ecopovtrng  6913  infglbti  7372  difinfsnlem  7446  enq0tr  7808  addnqprl  7903  addnqpru  7904  mulnqprl  7942  mulnqpru  7943  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemdisj  8025  mulextsr1lem  8154  pitonn  8222  rereceu  8263  cnegexlem1  8509  ltadd2  8755  eqord2  8820  mulext  8951  mulgt1  9202  lt2halves  9553  addltmul  9554  nzadd  9709  ltsubnn0  9724  zextlt  9750  recnz  9751  zeo  9763  peano5uzti  9766  irradd  10063  irrmul  10065  xltneg  10256  xleadd1  10295  icc0r  10346  fznuz  10527  uznfz  10528  facndiv  11200  hashf1  11310  ccatalpha  11404  swrdccatin2  11524  swrdccatin2d  11539  rennim  11791  abs00ap  11851  absle  11879  cau3lem  11904  caubnd2  11907  climshft  12096  subcn2  12103  mulcn2  12104  serf0  12144  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  efieq1re  12565  moddvds  12592  dvdsssfz1  12645  nn0seqcvgd  12845  algcvgblem  12853  eucalglt  12861  lcmgcdlem  12881  rpmul  12902  divgcdcoprm0  12905  isprm6  12952  rpexp  12958  eulerthlema  13038  eulerthlemh  13039  prmdiv  13043  pcprendvds2  13100  pcz  13141  pcprmpw  13143  pcadd2  13150  pcfac  13159  expnprm  13162  imasgrp2  13973  issubg4m  14056  znidomb  15103  tgss3  15316  cnpnei  15457  cnntr  15463  hmeoopn  15549  hmeocld  15550  mulcncflem  15845  plycolemc  15996  sincosq3sgn  16067  sincosq4sgn  16068  sineq0re  16088  chtqub  16308  perfect1  16310  lgsdir2lem4  16367  lgsne0  16374  lgsquad2lem2  16418  2sqlem8a  16458  clwwlkext2edg  16880  bj-peano4  17198  iswomni0  17320