Theorem ad2ant2r 513

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  fundif  5425  foco  5626  fvco4  5777  fliftfun  6002  f1imaen2g  7080  fodju0  7487  mulcomnqg  7750  mulassnqg  7751  ltdcnq  7764  lt2addnq  7771  lt2mulnq  7772  enq0ref  7800  enq0tr  7801  addcmpblnq0  7810  nqpnq0nq  7820  nqnq0m  7822  mulcomnq0  7827  addlocpr  7903  nqprl  7918  nqpru  7919  prmuloc  7933  distrlem1prl  7949  distrlem1pru  7950  ltaddpr  7964  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  caucvgprprlemopu  8066  addcomsrg  8122  mulcomsrg  8124  mulasssrg  8125  distrsrg  8126  addcnsr  8201  mulcnsr  8202  addcnsrec  8209  axaddcl  8231  axaddcom  8237  addsub4  8569  muladd  8711  mullt0  8808  apreim  8931  mulge0  8947  divmuldivap  9042  divmul24ap  9046  divmuleqap  9047  recdivap  9048  divadddivap  9057  conjmulap  9059  prodgt0gt0  9181  ltmul12a  9190  lemul12b  9191  lediv2a  9225  qmulcl  10037  irrmul  10047  xrrege0  10227  ge0addcl  10383  ge0mulcl  10384  ge0xaddcl  10385  fzass4  10468  fzrev  10491  fzocatel  10617  expclzaplem  11000  expge0  11012  expge1  11013  lt2sq  11050  le2sq  11051  bernneq  11098  sq11ap  11145  ccatw2s1p1g  11413  ccatw2s1p2  11414  swrdccatin2  11501  sqrt11ap  11804  2clim  12067  climge0  12091  tanaddaplem  12505  opeo  12664  omeo  12665  cncongr1  12881  pcpremul  13072  pcmul  13080  ennnfonelemf1  13309  setscom  13392  dfgrp3mlem  13903  grplactcnv  13907  issubg4m  13996  resgrpisgrp  13998  ghmpreima  14069  ghmeql  14070  conjghm  14079  rngpropd  14254  lmodprop2d  14685  opnneissb  15256  cncnpi  15329  neitx  15369  txcnmpt  15374  txrest  15377  txdis1cn  15379  ptolemy  15925  cxplt3  16022  cxple3  16023  lgslem3  16121  lgsdir2  16152  lgsne0  16157  lgsquad3  16203  umgr2edg  16448  umgrvad2edg  16452  wlkeq  16595  clwwlkccatlem  16641