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 4070  omwordri 4203  ltexpq 5080  mulcmpblnr 5183  cnegext 5348  muladdt 5421  divadddivt 5784  divdivdivt 5785  lemul12ait 5842  lemul12itOLD 5843  qaddclt 6269  fsumdivc 7035  fsumdivcALT 7036  2climnn 7102  2climnn0 7103  climmullem5 7124  climsqueeze 7140  climsqueeze2 7141  ser1f0 7170  iscau3 7938  iscau4 7940  metelcls 7965  metcnp4lem2 7969  metcn4i 7972  grpidinvlem3 8050  grpideu 8053  grprcan 8063  spwpr3OLD 8662  3oalem2 9608  hmopst 9945  adjaddt 10026  mdslmd4 10260  mdexch 10262  mdsymlem1 10330

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