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 4219  sbthlem8 4454  unidom 4808  cnegextlem3 5347  fsequb2 6524  caubnd 6926  climcau 7156  cvgcmp3c 7186  reccnv 7218  metcnp 7887  metcnss 7898  xpcn 7976  grpidinvlem3 8050  sm1cnilem 8347  nmoub3i 8436  blocni 8465  minveclem9 8553  hhlno 9826  nlelch 9994  riesz3 9995  kbass5t 10053  csmdsym 10261

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