Theorem ad2ant2l 408

Description: Deduction adding two conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant2.1	|- ((ph /\ ps) -> ch)

Assertion

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

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	adantrl 394	. 2 |- ((ph /\ (ta /\ ps)) -> ch)
3	2	adantll 392	1 |- (((th /\ ph) /\ (ta /\ ps)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  oaass 4179  xpdom2 4422  addcmpblnq 5024  addpipq 5026  addclpq 5030  addasspq 5035  distrpq 5039  ltsopq 5047  addcanpr 5124  ltsosr 5175  add42t 5311  muladdt 5393  mulsubt 5449  divmuldivt 5736  divmul24t 5739  divadddivt 5740  divdivdivt 5741  ltmul12it 5797  lemul12ait 5798  lemul12itOLD 5799  lemul12it 5800  zltp1let 6128  qaddclt 6207  iooint 6309  climaddc1 7054  climmullem3 7058  climsubc2 7067  climsup 7091  fctop 7592  cctop 7594  retopbas 7597  opnneissb 7669  nvcni 8266  minveclem18 8493  minveclem19 8494  minveclem21 8496  hvsub4t 8827  chocuni 9088  shscl 9196  osumlem3 9497  osumlem4 9498  5oalem2 9517  3oalem2 9525  hosub4t 9656  hmopst 9860  hmopmt 9861  hmopcot 9863  adjmult 9939  adjaddt 9940  mdslmd1lem1 10160  mdslmd1lem2 10161

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

Copyright terms: Public domain