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 4062  ordpipq 5036  prlem936b 5134  ltsrpr 5166  cnegext 5328  muladdt 5401  sub4t 5456  ltleaddt 5627  divadddivt 5748  divdivdivt 5749  ltmul12it 5805  qaddclt 6215  fzrevt 6451  facndivt 6888  fsumdivc 6981  fsumdivcALT 6982  opnuni 7820  tgioolem 7866  grpideu 8003  nvcni 8279  0lno 8395  ubthlem11 8483  ubthlem12 8484  hvaddsub4t 8884  bralnfnt 9811  hmopst 9883  hmopmt 9884  adjaddt 9964  kbass5t 9991  atoml 10246  irredlem2 10255  atcvat3 10260  mdsymlem5 10271  cdj1 10294

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