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 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  dvelimdf  2076  ceqsalt  2848  sbceqal  3107  csbiebt  3187  rspcsbela  3207  preqr1g  3889  repizf2  4297  copsexg  4382  onun2  4635  suc11g  4702  elrnrexdm  5841  isoselem  6020  riotass2  6061  oawordriexmid  6737  nnm00  6797  ecopovtrn  6900  ecopovtrng  6903  infglbti  7359  difinfsnlem  7433  enq0tr  7795  addnqprl  7890  addnqpru  7891  mulnqprl  7929  mulnqpru  7930  recexprlemss1l  7996  recexprlemss1u  7997  cauappcvgprlemdisj  8012  mulextsr1lem  8141  pitonn  8209  rereceu  8250  cnegexlem1  8495  ltadd2  8741  eqord2  8806  mulext  8936  mulgt1  9187  lt2halves  9524  addltmul  9525  nzadd  9680  ltsubnn0  9695  zextlt  9721  recnz  9722  zeo  9734  peano5uzti  9737  irradd  10029  irrmul  10030  xltneg  10221  xleadd1  10260  icc0r  10311  fznuz  10492  uznfz  10493  facndiv  11160  hashf1  11270  ccatalpha  11364  swrdccatin2  11484  swrdccatin2d  11499  rennim  11751  abs00ap  11811  absle  11838  cau3lem  11863  caubnd2  11866  climshft  12053  subcn2  12060  mulcn2  12061  serf0  12101  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  efieq1re  12522  moddvds  12549  dvdsssfz1  12602  nn0seqcvgd  12802  algcvgblem  12810  eucalglt  12818  lcmgcdlem  12838  rpmul  12859  divgcdcoprm0  12862  isprm6  12908  rpexp  12914  eulerthlema  12991  eulerthlemh  12992  prmdiv  12996  pcprendvds2  13053  pcz  13094  pcprmpw  13096  pcadd2  13103  pcfac  13112  expnprm  13115  imasgrp2  13896  issubg4m  13979  znidomb  14976  tgss3  15162  cnpnei  15303  cnntr  15309  hmeoopn  15395  hmeocld  15396  mulcncflem  15691  plycolemc  15842  sincosq3sgn  15912  sincosq4sgn  15913  perfect1  16095  lgsdir2lem4  16133  lgsne0  16140  lgsquad2lem2  16184  2sqlem8a  16224  clwwlkext2edg  16646  bj-peano4  16964  iswomni0  17075