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  3059  opeldmg  4931  elreldm  4953  ssimaex  5700  resflem  5804  f1eqcocnv  5924  fliftfun  5929  isopolem  5955  isosolem  5957  brtposg  6411  issmo2  6446  nnmcl  6640  nnawordi  6674  nnmordi  6675  nnmord  6676  swoord1  6722  ecopovtrn  6792  ecopovtrng  6795  f1domg  6922  mapen  7020  mapxpen  7022  supmoti  7176  isotilem  7189  exmidomniim  7324  enq0tr  7637  prubl  7689  ltexprlemloc  7810  addextpr  7824  recexprlem1ssl  7836  recexprlem1ssu  7837  cauappcvgprlemdisj  7854  mulcmpblnr  7944  mulgt0sr  7981  map2psrprg  8008  ltleletr  8244  ltle  8250  ltadd2  8582  leltadd  8610  reapti  8742  apreap  8750  reapcotr  8761  apcotr  8770  addext  8773  mulext1  8775  zapne  9537  zextle  9554  prime  9562  uzin  9772  indstr  9805  supinfneg  9807  infsupneg  9808  ublbneg  9825  xrltle  10011  xrre2  10034  icc0r  10139  fzrevral  10318  flqge  10519  modqadd1  10600  modqmul1  10616  facdiv  10977  elfzelfzccat  11153  resqrexlemgt0  11552  abs00ap  11594  absext  11595  climshftlemg  11834  climcaucn  11883  dvds2lem  12335  dvdsfac  12392  ltoddhalfle  12425  ndvdsadd  12463  bitsinv1lem  12493  gcdaddm  12526  bezoutlembi  12547  gcdzeq  12564  algcvga  12594  rpdvds  12642  cncongr1  12646  cncongr2  12647  prmind2  12663  euclemma  12689  isprm6  12690  rpexp  12696  sqrt2irr  12705  odzdvds  12789  pclemub  12831  pceulem  12838  pc2dvds  12874  fldivp1  12892  infpnlem1  12903  prmunb  12906  issubg4m  13751  imasabl  13894  fiinbas  14744  bastg  14756  tgcl  14759  opnssneib  14851  tgcnp  14904  iscnp4  14913  cnntr  14920  cnptopresti  14933  lmss  14941  lmtopcnp  14945  txdis  14972  xblss2ps  15099  xblss2  15100  blsscls2  15188  metequiv2  15191  bdxmet  15196  mulc1cncf  15284  cncfco  15286  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  lgsdir  15735  lgsquadlem2  15778  2sqlem8a  15822  2sqlem10  15825  uspgrushgr  15999  uspgrupgr  16000  usgruspgr  16002  clwwlkccatlem  16169  triap  16511