Theorem sylibd 149

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
sylibd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	2	biimpd 144	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3d  202  dvelimdf  2076  ceqsalt  2848  sbceqal  3107  csbiebt  3187  rspcsbela  3207  preqr1g  3891  repizf2  4299  copsexg  4384  onun2  4637  suc11g  4704  elrnrexdm  5847  isoselem  6026  riotass2  6067  oawordriexmid  6743  nnm00  6803  ecopovtrn  6906  ecopovtrng  6909  infglbti  7365  difinfsnlem  7439  enq0tr  7801  addnqprl  7896  addnqpru  7897  mulnqprl  7935  mulnqpru  7936  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemdisj  8018  mulextsr1lem  8147  pitonn  8215  rereceu  8256  cnegexlem1  8501  ltadd2  8747  eqord2  8812  mulext  8943  mulgt1  9194  lt2halves  9543  addltmul  9544  nzadd  9699  ltsubnn0  9714  zextlt  9740  recnz  9741  zeo  9753  peano5uzti  9756  irradd  10048  irrmul  10049  xltneg  10240  xleadd1  10279  icc0r  10330  fznuz  10511  uznfz  10512  facndiv  11179  hashf1  11289  ccatalpha  11383  swrdccatin2  11503  swrdccatin2d  11518  rennim  11770  abs00ap  11830  absle  11857  cau3lem  11882  caubnd2  11885  climshft  12072  subcn2  12079  mulcn2  12080  serf0  12120  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  efieq1re  12541  moddvds  12568  dvdsssfz1  12621  nn0seqcvgd  12821  algcvgblem  12829  eucalglt  12837  lcmgcdlem  12857  rpmul  12878  divgcdcoprm0  12881  isprm6  12927  rpexp  12933  eulerthlema  13010  eulerthlemh  13011  prmdiv  13015  pcprendvds2  13072  pcz  13113  pcprmpw  13115  pcadd2  13122  pcfac  13131  expnprm  13134  imasgrp2  13915  issubg4m  13998  znidomb  14995  tgss3  15181  cnpnei  15322  cnntr  15328  hmeoopn  15414  hmeocld  15415  mulcncflem  15710  plycolemc  15861  sincosq3sgn  15932  sincosq4sgn  15933  perfect1  16118  lgsdir2lem4  16162  lgsne0  16169  lgsquad2lem2  16213  2sqlem8a  16253  clwwlkext2edg  16675  bj-peano4  16993  iswomni0  17113