Theorem 3ad2antl1 809

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
3ad2antl.1	|- ((ph /\ ch) -> th)

Assertion

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

Proof of Theorem 3ad2antl1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ((ph /\ ch) -> th)
2	1	adantlr 393	. 2 |- (((ph /\ ta) /\ ch) -> th)
3	2	3adantl2 804	1 |- (((ph /\ ps /\ ta) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  supxrre 6083  expord2t 6604  exple1t 6607  isummulc1ALT 7213  metcni2 7895  cncfmet 7905  xpcn 7976  nvcni 8329  nvcni2 8330  nvcni3 8331  lnoadd 8419  lnosub 8420  lnomul 8421  ghomf1olem 10396  11st22nd 10458

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  df-an 225  df-3an 777

Copyright terms: Public domain