Theorem sylibd 149

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

Hypotheses

Ref	Expression
sylibd.1	|- ( ph -> ( ps -> ch ) )
sylibd.2	|- ( ph -> ( ch <-> th ) )

Assertion

Ref	Expression
sylibd	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		sylibd.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	2	biimpd 144	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

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  3886  repizf2  4294  copsexg  4379  onun2  4632  suc11g  4699  elrnrexdm  5838  isoselem  6016  riotass2  6057  oawordriexmid  6733  nnm00  6793  ecopovtrn  6896  ecopovtrng  6899  infglbti  7355  difinfsnlem  7429  enq0tr  7791  addnqprl  7886  addnqpru  7887  mulnqprl  7925  mulnqpru  7926  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemdisj  8008  mulextsr1lem  8137  pitonn  8205  rereceu  8246  cnegexlem1  8491  ltadd2  8737  eqord2  8802  mulext  8932  mulgt1  9183  lt2halves  9520  addltmul  9521  nzadd  9676  ltsubnn0  9691  zextlt  9717  recnz  9718  zeo  9730  peano5uzti  9733  irradd  10025  irrmul  10026  xltneg  10217  xleadd1  10256  icc0r  10307  fznuz  10487  uznfz  10488  facndiv  11155  hashf1  11265  ccatalpha  11359  swrdccatin2  11479  swrdccatin2d  11494  rennim  11746  abs00ap  11806  absle  11833  cau3lem  11858  caubnd2  11861  climshft  12048  subcn2  12055  mulcn2  12056  serf0  12096  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  efieq1re  12517  moddvds  12544  dvdsssfz1  12597  nn0seqcvgd  12797  algcvgblem  12805  eucalglt  12813  lcmgcdlem  12833  rpmul  12854  divgcdcoprm0  12857  isprm6  12903  rpexp  12909  eulerthlema  12986  eulerthlemh  12987  prmdiv  12991  pcprendvds2  13048  pcz  13089  pcprmpw  13091  pcadd2  13098  pcfac  13107  expnprm  13110  imasgrp2  13890  issubg4m  13973  znidomb  14965  tgss3  15102  cnpnei  15243  cnntr  15249  hmeoopn  15335  hmeocld  15336  mulcncflem  15631  plycolemc  15782  sincosq3sgn  15852  sincosq4sgn  15853  perfect1  16026  lgsdir2lem4  16064  lgsne0  16071  lgsquad2lem2  16115  2sqlem8a  16155  clwwlkext2edg  16577  bj-peano4  16895  iswomni0  17006