Theorem sylanbrc 645

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylanbrc.1	|- (ph -> ps)
sylanbrc.2	|- (ph -> ch)
sylanbrc.3	|- (th <-> (ps /\ ch))

Assertion

Ref	Expression
sylanbrc	|- (ph -> th)

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 |- (ph -> ps)
2		sylanbrc.2	. . 3 |- (ph -> ch)
3	1, 2	jca 518	. 2 |- (ph -> (ps /\ ch))
4		sylanbrc.3	. 2 |- (th <-> (ps /\ ch))
5	3, 4	sylibr 203	1 |- (ph -> th)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  ecase23d  1285  sbequ1  1918  sb2  2023  sbn  2062  eqeu  3008  euind  3024  reuind  3040  eqssd  3290  ssrabdv  3346  psstr  3374  vfinnc  4472  nnpw1ex  4485  evenoddnnnul  4515  sfinltfin  4536  sfin111  4537  imainss  5043  ssdmrn  5100  fnprg  5154  fnco  5192  f00  5250  f1ss  5263  f1f1orn  5298  foimacnv  5304  fun11iun  5306  dff3  5421  foco2  5427  ffnfv  5428  ffvresb  5432  isoini2  5499  f1oiso  5500  fnoprabg  5586  fmpt  5693  fmpt2d  5696  f1od  5727  sod  5938  so0  5942  iserd  5943  enpw1  6063  ncspw1eu  6160  ltcpw1pwg  6203  nchoicelem17  6306  nchoice  6309  fnfrec  6321