Theorem sylibrd 169

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

Hypotheses

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

Assertion

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

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibrd.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	biimprd 158	. 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  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4d  203  sbciegft  3082  opeldmg  4988  elreldm  5010  ssimaex  5767  resflem  5875  f1eqcocnv  6000  fliftfun  6005  isopolem  6031  isosolem  6033  brtposg  6529  issmo2  6564  nnmcl  6758  nnawordi  6792  nnmordi  6793  nnmord  6794  swoord1  6840  ecopovtrn  6910  ecopovtrng  6913  f1domg  7049  mapen  7151  mapxpen  7153  mapunen  7156  supmoti  7340  isotilem  7353  exmidomniim  7488  enq0tr  7808  prubl  7860  ltexprlemloc  7981  addextpr  7995  recexprlem1ssl  8007  recexprlem1ssu  8008  cauappcvgprlemdisj  8025  mulcmpblnr  8115  mulgt0sr  8152  map2psrprg  8179  ltleletr  8414  ltle  8420  ltadd2  8755  leltadd  8783  reapti  8916  apreap  8924  reapcotr  8935  apcotr  8944  addext  8947  mulext1  8949  zapne  9731  zextle  9749  prime  9757  uzin  9972  indstr  10010  supinfneg  10012  infsupneg  10013  ublbneg  10030  xrltle  10218  xrre2  10241  icc0r  10346  fzrevral  10530  flqge  10737  flapge  10738  modqadd1  10820  modqmul1  10836  facdiv  11199  elfzelfzccat  11391  resqrexlemgt0  11809  abs00ap  11851  absext  11852  climshftlemg  12094  climcaucn  12143  dvds2lem  12596  dvdsfac  12653  ltoddhalfle  12686  ndvdsadd  12724  bitsinv1lem  12754  gcdaddm  12787  bezoutlembi  12808  gcdzeq  12825  algcvga  12855  rpdvds  12903  cncongr1  12907  cncongr2  12908  prmind2  12924  euclemma  12951  isprm6  12952  rpexp  12958  sqrt2irr  12967  odzdvds  13054  pclemub  13096  pceulem  13103  pc2dvds  13139  fldivp1  13157  infpnlem1  13168  prmunb  13171  ballotfilem7  13338  issubg4m  14056  imasabl  14231  fiinbas  15287  bastg  15299  tgcl  15302  opnssneib  15394  tgcnp  15447  iscnp4  15456  cnntr  15463  cnptopresti  15476  lmss  15484  lmtopcnp  15488  txdis  15515  xblss2ps  15642  xblss2  15643  blsscls2  15731  metequiv2  15734  bdxmet  15739  mulc1cncf  15827  cncfco  15829  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  chtublem  16307  chtqub  16308  bposlem1  16323  bposlem3  16325  bposlem7  16329  lgsdir  16371  lgsquadlem2  16414  2sqlem8a  16458  2sqlem10  16461  uspgrushgr  16638  uspgrupgr  16639  usgruspgr  16641  clwwlkccatlem  16858  lealltlt1  16968  lealltlt2  16969  triap  17296