Theorem ad2ant2l 410

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 396	. 2 |- ((ph /\ (ta /\ ps)) -> ch)
3	2	adantll 394	1 |- (((th /\ ph) /\ (ta /\ ps)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  oaass 4201  xpdom2 4448  addcmpblnq 5064  addpipq 5066  addclpq 5070  addasspq 5075  distrpq 5079  ltsopq 5087  addcanpr 5164  ltsosr 5215  add42t 5351  muladdt 5433  mulsubt 5489  divmuldivt 5782  divmul24t 5785  divadddivt 5786  divdivdivt 5787  ltmul12it 5843  lemul12ait 5844  lemul12itOLD 5845  lemul12it 5846  zltp1let 6183  qaddclt 6270  iooint 6373  climaddc1 7118  climmullem3 7122  climsubc2 7131  climsup 7155  fctopOLD 7647  cctop 7649  retopbas 7652  opnneissb 7725  nvcni 8325  nvcni2 8326  minveclem18 8558  minveclem19 8559  minveclem21 8561  hvsub4t 8901  chocuni 9167  shscl 9276  osumlem3 9575  osumlem4 9576  5oalem2 9595  3oalem2 9603  hosub4t 9734  hmopst 9940  hmopmt 9941  hmopcot 9943  adjmult 10020  adjaddt 10021  mdslmd1lem1 10247  mdslmd1lem2 10248

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