Theorem adantlrl 400

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adantl2.1	|- (((ph /\ ps) /\ ch) -> th)

Assertion

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

Proof of Theorem adantlrl

Step	Hyp	Ref	Expression
1		adantl2.1	. . . 4 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 378	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	a1d 12	. 2 |- (ph -> (ta -> (ps -> (ch -> th))))
4	3	imp42 369	1 |- (((ph /\ (ta /\ ps)) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  omlimcl 4215  odi 4216  oelim2 4228  prlem936b 5166  qbtwnre 6279  bccl2t 6971  acdc3lem 7487  acdclem 7495  metcnp 7884  metcnp3 7893  xplmi 7970  bcthlem27 8022  bcthlem28 8023  grprcan 8059  minveclem30 8570  minveclem31 8571  unoplint 9839  hmoplint 9861  nlelch 9989  superpos 10276

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

Copyright terms: Public domain