Theorem bi3ant 280

Description: Construct a bi-conditional in antecedent position. (Contributed by Wolf Lammen, 14-May-2013.)

Hypothesis

Ref	Expression
bi3ant.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
bi3ant	|- (((th -> ta) -> ph) -> (((ta -> th) -> ps) -> ((th <-> ta) -> ch)))

Proof of Theorem bi3ant

Step	Hyp	Ref	Expression
1		bi1 178	. . 3 |- ((th <-> ta) -> (th -> ta))
2	1	imim1i 54	. 2 |- (((th -> ta) -> ph) -> ((th <-> ta) -> ph))
3		bi2 189	. . 3 |- ((th <-> ta) -> (ta -> th))
4	3	imim1i 54	. 2 |- (((ta -> th) -> ps) -> ((th <-> ta) -> ps))
5		bi3ant.1	. . 3 |- (ph -> (ps -> ch))
6	5	imim3i 55	. 2 |- (((th <-> ta) -> ph) -> (((th <-> ta) -> ps) -> ((th <-> ta) -> ch)))
7	2, 4, 6	syl2im 34	1 |- (((th -> ta) -> ph) -> (((ta -> th) -> ps) -> ((th <-> ta) -> ch)))

Syntax hints:   -> wi 4   <-> wb 176

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

This theorem is referenced by:  bisym  281