Theorem ad2ant2r 500

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 470	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 468	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  5355  fvco4  5493  fliftfun  5697  f1imaen2g  6687  fodju0  7019  mulcomnqg  7191  mulassnqg  7192  ltdcnq  7205  lt2addnq  7212  lt2mulnq  7213  enq0ref  7241  enq0tr  7242  addcmpblnq0  7251  nqpnq0nq  7261  nqnq0m  7263  mulcomnq0  7268  addlocpr  7344  nqprl  7359  nqpru  7360  prmuloc  7374  distrlem1prl  7390  distrlem1pru  7391  ltaddpr  7405  ltexprlemopu  7411  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  caucvgprprlemopu  7507  addcomsrg  7563  mulcomsrg  7565  mulasssrg  7566  distrsrg  7567  addcnsr  7642  mulcnsr  7643  addcnsrec  7650  axaddcl  7672  axaddcom  7678  addsub4  8005  muladd  8146  mullt0  8242  apreim  8365  mulge0  8381  divmuldivap  8472  divmul24ap  8476  divmuleqap  8477  recdivap  8478  divadddivap  8487  conjmulap  8489  prodgt0gt0  8609  ltmul12a  8618  lemul12b  8619  lediv2a  8653  qmulcl  9429  irrmul  9439  xrrege0  9608  ge0addcl  9764  ge0mulcl  9765  ge0xaddcl  9766  fzass4  9842  fzrev  9864  fzocatel  9976  expclzaplem  10317  expge0  10329  expge1  10330  lt2sq  10366  le2sq  10367  bernneq  10412  sq11ap  10458  sqrt11ap  10810  2clim  11070  climge0  11094  tanaddaplem  11445  opeo  11594  omeo  11595  cncongr1  11784  ennnfonelemf1  11931  setscom  11999  opnneissb  12324  cncnpi  12397  neitx  12437  txcnmpt  12442  txrest  12445  txdis1cn  12447  ptolemy  12905