Theorem ad2ant2rl 411

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  caoprmo 4062  omwordri 4193  ltexpq 5060  mulcmpblnr 5163  cnegext 5328  muladdt 5401  divadddivt 5748  divdivdivt 5749  lemul12ait 5806  lemul12itOLD 5807  qaddclt 6215  fsumdivc 6981  fsumdivcALT 6982  2climnn 7047  2climnn0 7048  climmullem5 7068  climsqueeze 7084  climsqueeze2 7085  ser1f0 7114  iscau3 7890  iscau4 7892  metelcls 7916  metcnp4lem2 7919  metcn4i 7922  grpidinvlem3 8000  grpideu 8003  grprcan 8013  3oalem2 9548  hmopst 9883  adjaddt 9964  mdslmd4 10197  mdexch 10199  mdsymlem1 10267

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