Theorem ad2ant2rl 413

Description: Deduction adding two conjuncts to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem ad2ant2rl

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	adantrl 396	. 2 |- ((ph /\ (ta /\ ps)) -> ch)
3	2	adantlr 395	1 |- (((ph /\ th) /\ (ta /\ ps)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  caoprmo 4076  omwordri 4209  ltexpq 5092  mulcmpblnr 5195  cnegext 5360  muladdt 5433  divadddivt 5786  divdivdivt 5787  lemul12ait 5844  lemul12itOLD 5845  qaddclt 6270  fsumdivc 7035  fsumdivcALT 7036  2climnn 7102  2climnn0 7103  climmullem5 7124  climsqueeze 7140  climsqueeze2 7141  ser1f0 7170  iscau3 7935  iscau4 7937  metelcls 7962  metcnp4lem2 7966  metcn4i 7969  grpidinvlem3 8047  grpideu 8050  grprcan 8059  3oalem2 9603  hmopst 9940  adjaddt 10021  mdslmd4 10255  mdexch 10257  mdsymlem1 10325

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