Theorem ad2ant2r 509

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 479	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 477	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  fundif  5364  foco  5558  fvco4  5705  fliftfun  5919  f1imaen2g  6943  fodju0  7310  mulcomnqg  7566  mulassnqg  7567  ltdcnq  7580  lt2addnq  7587  lt2mulnq  7588  enq0ref  7616  enq0tr  7617  addcmpblnq0  7626  nqpnq0nq  7636  nqnq0m  7638  mulcomnq0  7643  addlocpr  7719  nqprl  7734  nqpru  7735  prmuloc  7749  distrlem1prl  7765  distrlem1pru  7766  ltaddpr  7780  ltexprlemopu  7786  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemrl  7793  ltexprlemru  7795  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  caucvgprprlemopu  7882  addcomsrg  7938  mulcomsrg  7940  mulasssrg  7941  distrsrg  7942  addcnsr  8017  mulcnsr  8018  addcnsrec  8025  axaddcl  8047  axaddcom  8053  addsub4  8385  muladd  8526  mullt0  8623  apreim  8746  mulge0  8762  divmuldivap  8855  divmul24ap  8859  divmuleqap  8860  recdivap  8861  divadddivap  8870  conjmulap  8872  prodgt0gt0  8994  ltmul12a  9003  lemul12b  9004  lediv2a  9038  qmulcl  9828  irrmul  9838  xrrege0  10017  ge0addcl  10173  ge0mulcl  10174  ge0xaddcl  10175  fzass4  10254  fzrev  10276  fzocatel  10400  expclzaplem  10780  expge0  10792  expge1  10793  lt2sq  10830  le2sq  10831  bernneq  10877  sq11ap  10924  ccatw2s1p2  11171  swrdccatin2  11256  sqrt11ap  11544  2clim  11807  climge0  11831  tanaddaplem  12244  opeo  12403  omeo  12404  cncongr1  12620  pcpremul  12811  pcmul  12819  ennnfonelemf1  12984  setscom  13067  dfgrp3mlem  13626  grplactcnv  13630  issubg4m  13725  resgrpisgrp  13727  ghmpreima  13798  ghmeql  13799  conjghm  13808  rngpropd  13913  lmodprop2d  14306  opnneissb  14823  cncnpi  14896  neitx  14936  txcnmpt  14941  txrest  14944  txdis1cn  14946  ptolemy  15492  cxplt3  15588  cxple3  15589  lgslem3  15675  lgsdir2  15706  lgsne0  15711  lgsquad3  15757  umgr2edg  15999  umgrvad2edg  16003