Theorem adantrlr 401

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantrlr

Step	Hyp	Ref	Expression
1		adantr2.1	. . . 4 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 377	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	a1dd 42	. 2 |- (ph -> (ps -> (ta -> (ch -> th))))
4	3	imp44 371	1 |- ((ph /\ ((ps /\ ta) /\ ch)) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  distrlem4pr 5130  lediv12it 5896  cvgratlem1 7250  lmss 7953  bopcnlem2 7982  lmcau 7996  bcthlem17 8015  bcthlem19 8017  bcthlem20 8018  bcthlem21 8019  bcthlem24 8022  bcthlem25 8023  bcthlem26 8024  abl4 8105  ubthlem8 8536  ubthlem9 8537  ubthlem11 8539  ubthlem12 8540  lnopcon 9963  lnfncon 9990  mdslmd3 10259  atom1d 10280

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