Theorem adantrlr 403

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 379	. . 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 5142  lediv12it 5898  cvgratlem1 7250  lmss 7950  bopcnlem2 7979  lmcau 7993  bcthlem17 8012  bcthlem19 8014  bcthlem20 8015  bcthlem21 8016  bcthlem24 8019  bcthlem25 8020  bcthlem26 8021  abl4 8101  ubthlem8 8532  ubthlem9 8533  ubthlem11 8535  ubthlem12 8536  lnopcon 9958  lnfncon 9985  mdslmd3 10254  atom1d 10275

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