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  4986  elreldm  5008  ssimaex  5764  resflem  5872  f1eqcocnv  5997  fliftfun  6002  isopolem  6028  isosolem  6030  brtposg  6525  issmo2  6560  nnmcl  6754  nnawordi  6788  nnmordi  6789  nnmord  6790  swoord1  6836  ecopovtrn  6906  ecopovtrng  6909  f1domg  7044  mapen  7146  mapxpen  7148  mapunen  7151  supmoti  7333  isotilem  7346  exmidomniim  7481  enq0tr  7801  prubl  7853  ltexprlemloc  7974  addextpr  7988  recexprlem1ssl  8000  recexprlem1ssu  8001  cauappcvgprlemdisj  8018  mulcmpblnr  8108  mulgt0sr  8145  map2psrprg  8172  ltleletr  8407  ltle  8413  ltadd2  8747  leltadd  8775  reapti  8908  apreap  8916  reapcotr  8927  apcotr  8936  addext  8939  mulext1  8941  zapne  9721  zextle  9739  prime  9747  uzin  9957  indstr  9995  supinfneg  9997  infsupneg  9998  ublbneg  10015  xrltle  10202  xrre2  10225  icc0r  10330  fzrevral  10514  flqge  10719  modqadd1  10800  modqmul1  10816  facdiv  11178  elfzelfzccat  11370  resqrexlemgt0  11788  abs00ap  11830  absext  11831  climshftlemg  12070  climcaucn  12119  dvds2lem  12572  dvdsfac  12629  ltoddhalfle  12662  ndvdsadd  12700  bitsinv1lem  12730  gcdaddm  12763  bezoutlembi  12784  gcdzeq  12801  algcvga  12831  rpdvds  12879  cncongr1  12883  cncongr2  12884  prmind2  12900  euclemma  12926  isprm6  12927  rpexp  12933  sqrt2irr  12942  odzdvds  13026  pclemub  13068  pceulem  13075  pc2dvds  13111  fldivp1  13129  infpnlem1  13140  prmunb  13143  ballotfilem7  13281  issubg4m  13998  imasabl  14142  fiinbas  15152  bastg  15164  tgcl  15167  opnssneib  15259  tgcnp  15312  iscnp4  15321  cnntr  15328  cnptopresti  15341  lmss  15349  lmtopcnp  15353  txdis  15380  xblss2ps  15507  xblss2  15508  blsscls2  15596  metequiv2  15599  bdxmet  15604  mulc1cncf  15692  cncfco  15694  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  lgsdir  16166  lgsquadlem2  16209  2sqlem8a  16253  2sqlem10  16256  uspgrushgr  16433  uspgrupgr  16434  usgruspgr  16436  clwwlkccatlem  16653  lealltlt1  16763  lealltlt2  16764  triap  17090