Theorem 3adantl3 805

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl3

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

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

This theorem is referenced by:  3adantr3 808  fvco 3774  divdiv23t 5792  ltdiv23t 5892  lediv23t 5893  lediv2it 5897  iooss1 6373  ioojoint 6416  expord2t 6604  exple1t 6607  climrecl 7110  climge0 7112  climmullem3 7122  elcls 7704  cnco 7768  dnsconst 7788  metxplem4 7833  elbl2 7839  bl2in 7843  metcnss2 7899  lmuni 7951  lmle 7960  nvmul0or 8272  nvlmle 8333  fh1t 9561  fh2t 9562  cm2jt 9563  pjoi0t 9662  hoadddit 9729  hmopcot 9948

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 777

Copyright terms: Public domain