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  5374  foco  5570  fvco4  5718  fliftfun  5936  f1imaen2g  6966  fodju0  7345  mulcomnqg  7602  mulassnqg  7603  ltdcnq  7616  lt2addnq  7623  lt2mulnq  7624  enq0ref  7652  enq0tr  7653  addcmpblnq0  7662  nqpnq0nq  7672  nqnq0m  7674  mulcomnq0  7679  addlocpr  7755  nqprl  7770  nqpru  7771  prmuloc  7785  distrlem1prl  7801  distrlem1pru  7802  ltaddpr  7816  ltexprlemopu  7822  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  caucvgprprlemopu  7918  addcomsrg  7974  mulcomsrg  7976  mulasssrg  7977  distrsrg  7978  addcnsr  8053  mulcnsr  8054  addcnsrec  8061  axaddcl  8083  axaddcom  8089  addsub4  8421  muladd  8562  mullt0  8659  apreim  8782  mulge0  8798  divmuldivap  8891  divmul24ap  8895  divmuleqap  8896  recdivap  8897  divadddivap  8906  conjmulap  8908  prodgt0gt0  9030  ltmul12a  9039  lemul12b  9040  lediv2a  9074  qmulcl  9870  irrmul  9880  xrrege0  10059  ge0addcl  10215  ge0mulcl  10216  ge0xaddcl  10217  fzass4  10296  fzrev  10318  fzocatel  10443  expclzaplem  10824  expge0  10836  expge1  10837  lt2sq  10874  le2sq  10875  bernneq  10921  sq11ap  10968  ccatw2s1p1g  11221  ccatw2s1p2  11222  swrdccatin2  11309  sqrt11ap  11598  2clim  11861  climge0  11885  tanaddaplem  12298  opeo  12457  omeo  12458  cncongr1  12674  pcpremul  12865  pcmul  12873  ennnfonelemf1  13038  setscom  13121  dfgrp3mlem  13680  grplactcnv  13684  issubg4m  13779  resgrpisgrp  13781  ghmpreima  13852  ghmeql  13853  conjghm  13862  rngpropd  13967  lmodprop2d  14361  opnneissb  14878  cncnpi  14951  neitx  14991  txcnmpt  14996  txrest  14999  txdis1cn  15001  ptolemy  15547  cxplt3  15643  cxple3  15644  lgslem3  15730  lgsdir2  15761  lgsne0  15766  lgsquad3  15812  umgr2edg  16057  umgrvad2edg  16061  wlkeq  16204  clwwlkccatlem  16250