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  3061  opeldmg  4938  elreldm  4960  ssimaex  5710  resflem  5814  f1eqcocnv  5937  fliftfun  5942  isopolem  5968  isosolem  5970  brtposg  6425  issmo2  6460  nnmcl  6654  nnawordi  6688  nnmordi  6689  nnmord  6690  swoord1  6736  ecopovtrn  6806  ecopovtrng  6809  f1domg  6936  mapen  7037  mapxpen  7039  supmoti  7197  isotilem  7210  exmidomniim  7345  enq0tr  7659  prubl  7711  ltexprlemloc  7832  addextpr  7846  recexprlem1ssl  7858  recexprlem1ssu  7859  cauappcvgprlemdisj  7876  mulcmpblnr  7966  mulgt0sr  8003  map2psrprg  8030  ltleletr  8266  ltle  8272  ltadd2  8604  leltadd  8632  reapti  8764  apreap  8772  reapcotr  8783  apcotr  8792  addext  8795  mulext1  8797  zapne  9559  zextle  9576  prime  9584  uzin  9794  indstr  9832  supinfneg  9834  infsupneg  9835  ublbneg  9852  xrltle  10038  xrre2  10061  icc0r  10166  fzrevral  10345  flqge  10548  modqadd1  10629  modqmul1  10645  facdiv  11006  elfzelfzccat  11186  resqrexlemgt0  11603  abs00ap  11645  absext  11646  climshftlemg  11885  climcaucn  11934  dvds2lem  12387  dvdsfac  12444  ltoddhalfle  12477  ndvdsadd  12515  bitsinv1lem  12545  gcdaddm  12578  bezoutlembi  12599  gcdzeq  12616  algcvga  12646  rpdvds  12694  cncongr1  12698  cncongr2  12699  prmind2  12715  euclemma  12741  isprm6  12742  rpexp  12748  sqrt2irr  12757  odzdvds  12841  pclemub  12883  pceulem  12890  pc2dvds  12926  fldivp1  12944  infpnlem1  12955  prmunb  12958  issubg4m  13803  imasabl  13946  fiinbas  14802  bastg  14814  tgcl  14817  opnssneib  14909  tgcnp  14962  iscnp4  14971  cnntr  14978  cnptopresti  14991  lmss  14999  lmtopcnp  15003  txdis  15030  xblss2ps  15157  xblss2  15158  blsscls2  15246  metequiv2  15249  bdxmet  15254  mulc1cncf  15342  cncfco  15344  sincosq2sgn  15580  sincosq3sgn  15581  sincosq4sgn  15582  lgsdir  15793  lgsquadlem2  15836  2sqlem8a  15880  2sqlem10  15883  uspgrushgr  16060  uspgrupgr  16061  usgruspgr  16063  clwwlkccatlem  16280  triap  16700