Theorem adantlll 396

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantlll

Step	Hyp	Ref	Expression
1		adantl2.1	. . . 4 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 376	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	a1i 8	. 2 |- (ta -> (ph -> (ps -> (ch -> th))))
4	3	imp41 368	1 |- ((((ta /\ ph) /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  oewordri 4209  sbthlem8 4440  unidom 4788  cnegextlem3 5327  fsequb2 6464  caubnd 6871  climcau 7100  cvgcmp3c 7130  reccnv 7161  metcnp 7839  metcnss 7850  xpcn 7926  grpidinvlem3 8000  sm1cnilem 8294  nmoub3i 8381  blocni 8409  minveclem9 8497  hhlno 9766  nlelch 9932  riesz3 9933  kbass5t 9991  csmdsym 10198

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