Theorem adantlrl 398

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 376	. . 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 4193  odi 4194  oelim2 4206  prlem936b 5126  qbtwnre 6216  bccl2t 6909  acdc3lem 7428  acdclem 7436  metcnp 7826  metcnp3 7835  xplmi 7907  bcthlem27 7959  bcthlem28 7960  grprcan 7997  minveclem30 8505  minveclem31 8506  unoplint 9760  hmoplint 9782  nlelch 9909  superpos 10189

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