Theorem 3ad2antl3 811

Description: Deduction adding conjuncts to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antl3

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ((ph /\ ch) -> th)
2	1	adantll 392	. 2 |- (((ta /\ ph) /\ ch) -> th)
3	2	3adantl1 803	1 |- (((ps /\ ta /\ ph) /\ ch) -> th)

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

This theorem is referenced by:  oprabval6g 4032  lemul1t 5832  lediv1tOLD 5852  climrecl 7110  elcls 7704  ssblex 7856  metcnp2 7888  cncfmet 7905  metcnp4 7970  hoadddit 9729  kbmult 9879  kbass2t 10050  elo 10444  idmon 10745

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