Theorem adantlrr 399

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantlrr

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  tfrlem2 3903  oelim 4159  odi 4200  supmo 4556  cnegext 5328  divexpt 6538  expmwordit 6545  climaddlem3 7060  climmullem3 7066  ser1cmp2 7121  cvgratlem2 7194  islp2 7697  blss 7805  ssblex 7808  lmss 7904  lmle 7911  xplmi 7923  cmsss 7947  blocnilem 8408  ubthlem3 8475  ubthlem11 8483  superpos 10218  irredlem2 10255

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