Theorem 3imtr3d 541

Description: More general version of 3imtr3 218. Useful for converting conditional definitions in a formula.

Hypotheses

Ref	Expression
3imtr3d.1	|- (ph -> (ps -> ch))
3imtr3d.2	|- (ph -> (ps <-> th))
3imtr3d.3	|- (ph -> (ch <-> ta))

Assertion

Ref	Expression
3imtr3d	|- (ph -> (th -> ta))

Proof of Theorem 3imtr3d

Step	Hyp	Ref	Expression
1		3imtr3d.2	. 2 |- (ph -> (ps <-> th))
2		3imtr3d.1	. . 3 |- (ph -> (ps -> ch))
3		3imtr3d.3	. . 3 |- (ph -> (ch <-> ta))
4	2, 3	sylibd 202	. 2 |- (ph -> (ps -> ta))
5	1, 4	sylbird 205	1 |- (ph -> (th -> ta))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  dvelimdf 1249  hbeqd 1909  hbeld 1910  hbsbc1gd 1979  hbsbcgd 1980  hbcsb1gd 2023  hbcsbgd 2024  uniiunlem 2128  hbopd 2493  hbbrd 2654  hbimad 3404  fornex 3670  hbfvd 3721  hbfvd2 3722  hboprd 3973  sdomel 4827  cardsdomel 4832  ltapr 5131  hbnegd 5343  nnleltp1t 5909  om2uzlt2 6244  metdnsconst 7853  tgioo 7867  cmsss 7947  sincosq1sgn 8640  sincosq2sgn 8641  efif1lem4 8667  pjnormss 10034

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain