Theorem adantlrr 401

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 378	. . 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 3918  oelim 4175  odi 4216  supmo 4585  cnegext 5360  divexpt 6600  expmwordit 6607  climaddlem3 7116  climmullem3 7122  ser1cmp2 7177  cvgratlem2 7251  islp2 7744  blss 7850  ssblex 7853  lmss 7950  lmle 7957  xplmi 7970  cmsss 7994  blocnilem 8460  ubthlem3 8527  ubthlem11 8535  superpos 10276  irredlem2 10313

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