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  3076  opeldmg  4966  elreldm  4988  ssimaex  5743  resflem  5846  f1eqcocnv  5970  fliftfun  5975  isopolem  6001  isosolem  6003  brtposg  6498  issmo2  6533  nnmcl  6727  nnawordi  6761  nnmordi  6762  nnmord  6763  swoord1  6809  ecopovtrn  6879  ecopovtrng  6882  f1domg  7010  mapen  7112  mapxpen  7114  mapunen  7117  supmoti  7297  isotilem  7310  exmidomniim  7445  enq0tr  7765  prubl  7817  ltexprlemloc  7938  addextpr  7952  recexprlem1ssl  7964  recexprlem1ssu  7965  cauappcvgprlemdisj  7982  mulcmpblnr  8072  mulgt0sr  8109  map2psrprg  8136  ltleletr  8371  ltle  8377  ltadd2  8711  leltadd  8739  reapti  8871  apreap  8879  reapcotr  8890  apcotr  8899  addext  8902  mulext1  8904  zapne  9672  zextle  9690  prime  9698  uzin  9908  indstr  9946  supinfneg  9948  infsupneg  9949  ublbneg  9966  xrltle  10153  xrre2  10176  icc0r  10281  fzrevral  10464  flqge  10669  modqadd1  10750  modqmul1  10766  facdiv  11128  elfzelfzccat  11316  resqrexlemgt0  11733  abs00ap  11775  absext  11776  climshftlemg  12015  climcaucn  12064  dvds2lem  12517  dvdsfac  12574  ltoddhalfle  12607  ndvdsadd  12645  bitsinv1lem  12675  gcdaddm  12708  bezoutlembi  12729  gcdzeq  12746  algcvga  12776  rpdvds  12824  cncongr1  12828  cncongr2  12829  prmind2  12845  euclemma  12871  isprm6  12872  rpexp  12878  sqrt2irr  12887  odzdvds  12971  pclemub  13013  pceulem  13020  pc2dvds  13056  fldivp1  13074  infpnlem1  13085  prmunb  13088  ballotfilem7  13226  issubg4m  13949  imasabl  14092  fiinbas  15043  bastg  15055  tgcl  15058  opnssneib  15150  tgcnp  15203  iscnp4  15212  cnntr  15219  cnptopresti  15232  lmss  15240  lmtopcnp  15244  txdis  15271  xblss2ps  15398  xblss2  15399  blsscls2  15487  metequiv2  15490  bdxmet  15495  mulc1cncf  15583  cncfco  15585  sincosq2sgn  15821  sincosq3sgn  15822  sincosq4sgn  15823  lgsdir  16037  lgsquadlem2  16080  2sqlem8a  16124  2sqlem10  16127  uspgrushgr  16304  uspgrupgr  16305  usgruspgr  16307  clwwlkccatlem  16524  lealltlt1  16634  lealltlt2  16635  triap  16952