Theorem adantrrr 403

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantrrr

Step	Hyp	Ref	Expression
1		adantr2.1	. . . 4 |- ((ph /\ (ps /\ ch)) -> th)
2	1	a1d 12	. . 3 |- ((ph /\ (ps /\ ch)) -> (ta -> th))
3	2	exp32 377	. 2 |- (ph -> (ps -> (ch -> (ta -> th))))
4	3	imp45 372	1 |- ((ph /\ (ps /\ (ch /\ ta))) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  supmo 4556  zorn2lem6 4773  lemul12ait 5806  lediv12it 5852  climsqueeze 7084  climsqueeze2 7085  caucvglem6 7106  cvgratlem1 7193  tgclt 7574  tgss2t 7587  neissex 7688  opni3 7818  iscau3 7890  iscau4 7892  bopcnlem2 7932  bcthlem17 7965  abl4 8056  ubthlem12 8484  shscl 9219  nlelch 9932  mdslmd3 10196

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