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  3008  opeldmg  4850  elreldm  4871  ssimaex  5598  resflem  5701  f1eqcocnv  5813  fliftfun  5818  isopolem  5844  isosolem  5846  brtposg  6279  issmo2  6314  nnmcl  6506  nnawordi  6540  nnmordi  6541  nnmord  6542  swoord1  6588  ecopovtrn  6658  ecopovtrng  6661  f1domg  6784  mapen  6874  mapxpen  6876  supmoti  7022  isotilem  7035  exmidomniim  7169  enq0tr  7463  prubl  7515  ltexprlemloc  7636  addextpr  7650  recexprlem1ssl  7662  recexprlem1ssu  7663  cauappcvgprlemdisj  7680  mulcmpblnr  7770  mulgt0sr  7807  map2psrprg  7834  ltleletr  8069  ltle  8075  ltadd2  8406  leltadd  8434  reapti  8566  apreap  8574  reapcotr  8585  apcotr  8594  addext  8597  mulext1  8599  zapne  9357  zextle  9374  prime  9382  uzin  9590  indstr  9623  supinfneg  9625  infsupneg  9626  ublbneg  9643  xrltle  9828  xrre2  9851  icc0r  9956  fzrevral  10135  flqge  10313  modqadd1  10392  modqmul1  10408  facdiv  10750  resqrexlemgt0  11061  abs00ap  11103  absext  11104  climshftlemg  11342  climcaucn  11391  dvds2lem  11842  dvdsfac  11898  ltoddhalfle  11930  ndvdsadd  11968  gcdaddm  12017  bezoutlembi  12038  gcdzeq  12055  algcvga  12083  rpdvds  12131  cncongr1  12135  cncongr2  12136  prmind2  12152  euclemma  12178  isprm6  12179  rpexp  12185  sqrt2irr  12194  odzdvds  12277  pclemub  12319  pceulem  12326  pc2dvds  12362  fldivp1  12380  infpnlem1  12391  prmunb  12394  issubg4m  13132  imasabl  13273  fiinbas  14006  bastg  14018  tgcl  14021  opnssneib  14113  tgcnp  14166  iscnp4  14175  cnntr  14182  cnptopresti  14195  lmss  14203  lmtopcnp  14207  txdis  14234  xblss2ps  14361  xblss2  14362  blsscls2  14450  metequiv2  14453  bdxmet  14458  mulc1cncf  14533  cncfco  14535  sincosq2sgn  14705  sincosq3sgn  14706  sincosq4sgn  14707  lgsdir  14894  2sqlem8a  14927  2sqlem10  14930  triap  15236