Theorem sylibrd 168

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 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  sbciegft  2981  opeldmg  4809  elreldm  4830  ssimaex  5547  resflem  5649  f1eqcocnv  5759  fliftfun  5764  isopolem  5790  isosolem  5792  brtposg  6222  issmo2  6257  nnmcl  6449  nnawordi  6483  nnmordi  6484  nnmord  6485  swoord1  6530  ecopovtrn  6598  ecopovtrng  6601  f1domg  6724  mapen  6812  mapxpen  6814  supmoti  6958  isotilem  6971  exmidomniim  7105  enq0tr  7375  prubl  7427  ltexprlemloc  7548  addextpr  7562  recexprlem1ssl  7574  recexprlem1ssu  7575  cauappcvgprlemdisj  7592  mulcmpblnr  7682  mulgt0sr  7719  map2psrprg  7746  ltleletr  7980  ltle  7986  ltadd2  8317  leltadd  8345  reapti  8477  apreap  8485  reapcotr  8496  apcotr  8505  addext  8508  mulext1  8510  zapne  9265  zextle  9282  prime  9290  uzin  9498  indstr  9531  supinfneg  9533  infsupneg  9534  ublbneg  9551  xrltle  9734  xrre2  9757  icc0r  9862  fzrevral  10040  flqge  10217  modqadd1  10296  modqmul1  10312  facdiv  10651  resqrexlemgt0  10962  abs00ap  11004  absext  11005  climshftlemg  11243  climcaucn  11292  dvds2lem  11743  dvdsfac  11798  ltoddhalfle  11830  ndvdsadd  11868  gcdaddm  11917  bezoutlembi  11938  gcdzeq  11955  algcvga  11983  rpdvds  12031  cncongr1  12035  cncongr2  12036  prmind2  12052  euclemma  12078  isprm6  12079  rpexp  12085  sqrt2irr  12094  odzdvds  12177  pclemub  12219  pceulem  12226  pc2dvds  12261  fldivp1  12278  infpnlem1  12289  prmunb  12292  fiinbas  12697  bastg  12711  tgcl  12714  opnssneib  12806  tgcnp  12859  iscnp4  12868  cnntr  12875  cnptopresti  12888  lmss  12896  lmtopcnp  12900  txdis  12927  xblss2ps  13054  xblss2  13055  blsscls2  13143  metequiv2  13146  bdxmet  13151  mulc1cncf  13226  cncfco  13228  sincosq2sgn  13398  sincosq3sgn  13399  sincosq4sgn  13400  lgsdir  13586  2sqlem8a  13608  2sqlem10  13611  triap  13918