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 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4d  203  sbciegft  3062  opeldmg  4936  elreldm  4958  ssimaex  5707  resflem  5811  f1eqcocnv  5932  fliftfun  5937  isopolem  5963  isosolem  5965  brtposg  6420  issmo2  6455  nnmcl  6649  nnawordi  6683  nnmordi  6684  nnmord  6685  swoord1  6731  ecopovtrn  6801  ecopovtrng  6804  f1domg  6931  mapen  7032  mapxpen  7034  supmoti  7192  isotilem  7205  exmidomniim  7340  enq0tr  7654  prubl  7706  ltexprlemloc  7827  addextpr  7841  recexprlem1ssl  7853  recexprlem1ssu  7854  cauappcvgprlemdisj  7871  mulcmpblnr  7961  mulgt0sr  7998  map2psrprg  8025  ltleletr  8261  ltle  8267  ltadd2  8599  leltadd  8627  reapti  8759  apreap  8767  reapcotr  8778  apcotr  8787  addext  8790  mulext1  8792  zapne  9554  zextle  9571  prime  9579  uzin  9789  indstr  9827  supinfneg  9829  infsupneg  9830  ublbneg  9847  xrltle  10033  xrre2  10056  icc0r  10161  fzrevral  10340  flqge  10543  modqadd1  10624  modqmul1  10640  facdiv  11001  elfzelfzccat  11178  resqrexlemgt0  11582  abs00ap  11624  absext  11625  climshftlemg  11864  climcaucn  11913  dvds2lem  12366  dvdsfac  12423  ltoddhalfle  12456  ndvdsadd  12494  bitsinv1lem  12524  gcdaddm  12557  bezoutlembi  12578  gcdzeq  12595  algcvga  12625  rpdvds  12673  cncongr1  12677  cncongr2  12678  prmind2  12694  euclemma  12720  isprm6  12721  rpexp  12727  sqrt2irr  12736  odzdvds  12820  pclemub  12862  pceulem  12869  pc2dvds  12905  fldivp1  12923  infpnlem1  12934  prmunb  12937  issubg4m  13782  imasabl  13925  fiinbas  14776  bastg  14788  tgcl  14791  opnssneib  14883  tgcnp  14936  iscnp4  14945  cnntr  14952  cnptopresti  14965  lmss  14973  lmtopcnp  14977  txdis  15004  xblss2ps  15131  xblss2  15132  blsscls2  15220  metequiv2  15223  bdxmet  15228  mulc1cncf  15316  cncfco  15318  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  lgsdir  15767  lgsquadlem2  15810  2sqlem8a  15854  2sqlem10  15857  uspgrushgr  16034  uspgrupgr  16035  usgruspgr  16037  clwwlkccatlem  16254  triap  16654