Theorem 3adantl2 804

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl2

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

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

This theorem is referenced by:  3adantr2 807  3ad2antl1 809  omord2 4198  oeord 4215  div23t 5742  div12t 5744  divsubdirtOLD 5775  divdiv23t 5792  lediv1tOLD 5852  lediv2it 5897  nndivt 5959  expsubt 6598  expord2t 6604  metxplem4 7833  bl2in 7843  metcnp2 7888  lmuni 7951  metcnp4 7970  metcn4i 7972  ipval2lem2 8354  ipval2lem5 8360  minveclem24 8568  minveclem25 8569  minveclem26 8570  pjspansnt 9500  fh1t 9561  cm2jt 9563  hoadddit 9729  hoadddirt 9730  kbmult 9879  homco2t 9901

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