Theorem ad2ant2lr 410

Description: Deduction adding two conjuncts to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	adantrr 395	. 2 |- ((ph /\ (ps /\ ta)) -> ch)
3	2	adantll 392	1 |- (((th /\ ph) /\ (ps /\ ta)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  caoprmo 4056  ordpipq 5028  prlem936b 5126  ltsrpr 5158  cnegext 5320  muladdt 5393  sub4t 5448  ltleaddt 5619  divadddivt 5740  divdivdivt 5741  ltmul12it 5797  qaddclt 6207  fzrevt 6443  facndivt 6880  fsumdivc 6973  fsumdivcALT 6974  opnuni 7808  tgioolem 7853  grpideu 7987  nvcni 8266  0lno 8382  ubthlem11 8470  ubthlem12 8471  hvaddsub4t 8866  bralnfnt 9788  hmopst 9860  hmopmt 9861  adjaddt 9940  kbass5t 9965  atoml 10217  irredlem2 10226  atcvat3 10231  mdsymlem5 10242  cdj1 10265

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