Theorem 3adantl3 804

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 798	. 2 |- ((ph /\ ps /\ ta) -> (ch -> th))
4	3	imp 350	1 |- (((ph /\ ps /\ ta) /\ ch) -> th)

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

This theorem is referenced by:  3adantr3 807  fvco 3765  divdiv23t 5756  ltdiv23t 5848  lediv23t 5849  lediv2it 5853  iooss1 6318  expord2t 6543  exple1t 6546  climrecl 7055  climge0 7057  climmullem3 7066  elcls 7654  cnco 7718  dnsconst 7738  metxplem4 7785  elbl2 7791  bl2in 7795  metcnss2 7851  lmuni 7902  lmle 7911  nvmul0or 8224  nvlmle 8281  fh1t 9501  fh2t 9502  cm2jt 9503  pjoi0t 9602  hoadddit 9669  hmopcot 9886

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