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 3912  oelim 4169  odi 4210  supmo 4576  cnegext 5348  divexpt 6599  expmwordit 6606  climaddlem3 7116  climmullem3 7122  ser1cmp2 7177  cvgratlem2 7251  islp2 7747  blss 7853  ssblex 7856  lmss 7953  lmle 7960  xplmi 7973  cmsss 7997  blocnilem 8464  ubthlem3 8531  ubthlem11 8539  superpos 10281  irredlem2 10318

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