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 4195  xpdom2 4442  addcmpblnq 5052  addpipq 5054  addclpq 5058  addasspq 5063  distrpq 5067  ltsopq 5075  addcanpr 5152  ltsosr 5203  add42t 5339  muladdt 5421  mulsubt 5477  divmuldivt 5780  divmul24t 5783  divadddivt 5784  divdivdivt 5785  ltmul12it 5841  lemul12ait 5842  lemul12itOLD 5843  lemul12it 5844  zltp1let 6181  qaddclt 6269  iooint 6372  climaddc1 7118  climmullem3 7122  climsubc2 7131  climsup 7155  fctopOLD 7650  cctop 7652  retopbas 7655  opnneissb 7728  nvcni 8329  nvcni2 8330  minveclem18 8562  minveclem19 8563  minveclem21 8565  hvsub4t 8906  chocuni 9172  shscl 9281  osumlem3 9580  osumlem4 9581  5oalem2 9600  3oalem2 9608  hosub4t 9739  hmopst 9945  hmopmt 9946  hmopcot 9948  adjmult 10025  adjaddt 10026  mdslmd1lem1 10252  mdslmd1lem2 10253

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