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 1251  hbeqd 1911  hbeld 1912  hbsbc1gd 1981  hbsbcgd 1982  hbcsb1gd 2025  hbcsbgd 2026  uniiunlem 2130  hbopd 2495  hbbrd 2656  hbimad 3409  fornex 3676  hbfvd 3727  hbfvd2 3728  hboprd 3979  sdomel 4834  cardsdomel 4839  ltapr 5138  hbnegd 5350  nnleltp1t 5915  om2uzlt2 6254  metdnsconst 7884  tgioo 7898  cmsss 7980  sincosq1sgn 8685  sincosq2sgn 8686  efif1lem4 8712  pjnormss 10087

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