Theorem 3adantl1 802

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl1

Step	Hyp	Ref	Expression
1		3adantl.1	. . . 4 |- (((ph /\ ps) /\ ch) -> th)
2	1	ex 373	. . 3 |- ((ph /\ ps) -> (ch -> th))
3	2	3adant1 796	. 2 |- ((ta /\ ph /\ ps) -> (ch -> th))
4	3	imp 350	1 |- (((ta /\ ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774

This theorem is referenced by:  3adantr1 805  3ad2antl2 809  3ad2antl3 810  omord2 4188  oeord 4205  divasst 5712  div12t 5715  divsubdirt 5739  lediv1t 5814  lemuldivt 5832  ltdiv23t 5848  lediv23t 5849  iooss2 6319  elfz2nn0t 6435  fznn0subt 6438  expsubt 6537  climsqueeze 7084  climsqueeze2 7085  cnco 7718  metxplem4 7785  ssblex 7808  metcnss 7850  metcnp4 7920  nvcni 8279  fh2t 9502  homco1t 9667  homulasst 9668  hoadddit 9669  hoadddirt 9670  homco2t 9840

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  df-3an 776

Copyright terms: Public domain