Theorem ad2ant2r 501

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2r	⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Proof of Theorem ad2ant2r

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 471	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 469	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  foco  5414  fvco4  5552  fliftfun  5758  f1imaen2g  6750  fodju0  7102  mulcomnqg  7315  mulassnqg  7316  ltdcnq  7329  lt2addnq  7336  lt2mulnq  7337  enq0ref  7365  enq0tr  7366  addcmpblnq0  7375  nqpnq0nq  7385  nqnq0m  7387  mulcomnq0  7392  addlocpr  7468  nqprl  7483  nqpru  7484  prmuloc  7498  distrlem1prl  7514  distrlem1pru  7515  ltaddpr  7529  ltexprlemopu  7535  ltexprlemdisj  7538  ltexprlemloc  7539  ltexprlemrl  7542  ltexprlemru  7544  recexprlemloc  7563  recexprlem1ssl  7565  recexprlem1ssu  7566  caucvgprprlemopu  7631  addcomsrg  7687  mulcomsrg  7689  mulasssrg  7690  distrsrg  7691  addcnsr  7766  mulcnsr  7767  addcnsrec  7774  axaddcl  7796  axaddcom  7802  addsub4  8132  muladd  8273  mullt0  8369  apreim  8492  mulge0  8508  divmuldivap  8599  divmul24ap  8603  divmuleqap  8604  recdivap  8605  divadddivap  8614  conjmulap  8616  prodgt0gt0  8737  ltmul12a  8746  lemul12b  8747  lediv2a  8781  qmulcl  9566  irrmul  9576  xrrege0  9752  ge0addcl  9908  ge0mulcl  9909  ge0xaddcl  9910  fzass4  9987  fzrev  10009  fzocatel  10124  expclzaplem  10469  expge0  10481  expge1  10482  lt2sq  10518  le2sq  10519  bernneq  10564  sq11ap  10611  sqrt11ap  10966  2clim  11228  climge0  11252  tanaddaplem  11665  opeo  11819  omeo  11820  cncongr1  12014  pcpremul  12202  pcmul  12210  ennnfonelemf1  12288  setscom  12371  opnneissb  12696  cncnpi  12769  neitx  12809  txcnmpt  12814  txrest  12817  txdis1cn  12819  ptolemy  13286  cxplt3  13381  cxple3  13382