Theorem 3adantl2 802

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

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

This theorem is referenced by:  3adantr2 805  3ad2antl1 807  omord2 4182  oeord 4199  div23t 5705  div12t 5707  divsubdirt 5731  divdiv23t 5748  lediv1t 5806  lediv2it 5845  nndivt 5906  expsubt 6529  expord2t 6535  metxplem4 7773  bl2in 7783  metcnp2 7827  lmuni 7886  metcnp4 7904  metcn4i 7906  ipval2lem2 8288  ipval2lem5 8294  minveclem24 8499  minveclem25 8500  minveclem26 8501  pjspansnt 9417  fh1t 9478  cm2jt 9480  hoadddit 9646  hoadddirt 9647  kbmult 9795  homco2t 9817

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 775

Copyright terms: Public domain