Theorem adantrrr 405

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 379	. 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 4585  zorn2lem6 4803  lemul12ait 5844  lediv12it 5898  climsqueeze 7140  climsqueeze2 7141  caucvglem6 7162  cvgratlem1 7250  tgclt 7623  tgss2t 7636  neissex 7735  opni3 7863  iscau3 7935  iscau4 7937  bopcnlem2 7979  bcthlem17 8012  abl4 8101  ubthlem12 8536  shscl 9276  nlelch 9989  mdslmd3 10254

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