Theorem ad2ant2rl 494

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)

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

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  fvtp1g  5390  fcof1o  5449  addcomnqg  6571  addassnqg  6572  nqtri3or  6586  ltexnqq  6598  nqnq0pi  6628  nqpnq0nq  6643  nqnq0a  6644  addassnq0lemcl  6651  ltaddpr  6787  ltexprlemloc  6797  addcanprlemu  6805  recexprlem1ssu  6824  aptiprleml  6829  mulcomsrg  6934  mulasssrg  6935  distrsrg  6936  aptisr  6955  mulcnsr  7003  cnegex  7286  muladd  7488  lemul12b  7939  qaddcl  8720  iooshf  8975  elfzomelpfzo  9240  expnegzap  9510