Theorem 3anim3i 1055

Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypothesis

Ref	Expression
3animi.1	|- (ph -> ps)

Assertion

Ref	Expression
3anim3i	|- ((ch /\ th /\ ph) -> (ch /\ th /\ ps))

Proof of Theorem 3anim3i

Step	Hyp	Ref	Expression
1		id 73	. 2 |- (ch -> ch)
2		id 73	. 2 |- (th -> th)
3		3animi.1	. 2 |- (ph -> ps)
4	1, 2, 3	3anim123i 1053	1 |- ((ch /\ th /\ ph) -> (ch /\ th /\ ps))

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  findOLD 3978  elioo4g 7553  bnj556 13280  bnj557 13281  bnj1067 13399  bnj1145 13431  posprs 14581  sexptrt 15243  connsub 15443  reconn 15451

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 164  df-an 242  df-3an 860

Copyright terms: Public domain