Theorem adantllr 399

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantllr

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	imp41 368	1 |- ((((ph /\ ta) /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  oewordri 4225  cnegextlem3 5359  cnegext 5360  lemul12ait 5844  ser1add2 6339  expmwordit 6607  seq1ublem 6911  bccl2t 6971  fsumcmpndx2 7042  2climnn 7102  2climnn0 7103  climmullem3 7122  climcmpc1 7139  reccnv 7218  expcnv 7233  cvgratlem5 7254  fsum0diag3 7260  tgclt 7623  tgss2t 7636  neindisj 7728  iscncl 7767  blss 7850  metcnp 7884  lmle 7957  metelcls 7962  iscms2lem5 7990  bcthlem24 8019  bcthlem26 8021  grpidinvlem3 8047  grpideu 8050  grprcan 8059  blocni 8461  ubthlem3 8527  minveclem27 8567  minveclem28 8568  minveclem30 8570  minveclem31 8571  normcant 9494  pjspansnt 9495  unoplint 9839  hmoplint 9861  nmophm 9956  lnopcon 9958  lnfncon 9985  nlelch 9989  mdslmd3 10254  irredlem1 10312  irredlem2 10313  mdsymlem5 10329  cdj1 10355

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