Theorem bnj835 30829

Description: /\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj835.1	|- ( et <-> ( ph /\ ps /\ ch ) )
bnj835.2	|- ( ph -> ta )

Assertion

Ref	Expression
bnj835	|- ( et -> ta )

Proof of Theorem bnj835

Step	Hyp	Ref	Expression
1		bnj835.1	. 2 |- ( et <-> ( ph /\ ps /\ ch ) )
2		bnj835.2	. . 3 |- ( ph -> ta )
3	2	3ad2ant1 1082	. 2 |- ( ( ph /\ ps /\ ch ) -> ta )
4	1, 3	sylbi 207	1 |- ( et -> ta )

Syntax hints:   -> wi 4   <-> wb 196   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  bnj1219  30871  bnj1379  30901  bnj1175  31072  bnj1286  31087  bnj1280  31088  bnj1296  31089  bnj1398  31102  bnj1415  31106  bnj1417  31109  bnj1421  31110  bnj1442  31117  bnj1450  31118  bnj1452  31120  bnj1489  31124  bnj1312  31126  bnj1501  31135  bnj1523  31139