Theorem adantlll 405

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 385	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	a1i 8	. 2 |- (ta -> (ph -> (ps -> (ch -> th))))
4	3	imp41 375	1 |- ((((ta /\ ph) /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  oewordri 4277  sbthlem8 4517  unidom 4870  cnegexlem3 5412  fsequb2 6550  caubndi 7016  climcaui 7246  cvgcmp3ci 7276  reccnv 7308  metcnp 7972  metcnss 7983  xpcn 8061  grpidinvlem3 8135  sm1cnilem 8431  nmoub3i 8520  blocni 8549  minveclem9 8637  hhlnoi 9909  nlelchi 10077  riesz3i 10078  kbass5 10136  csmdsymi 10345

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 154  df-an 232

Copyright terms: Public domain