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  8570  muladd  8712  mullt0  8809  apreim  8933  mulge0  8949  divmuldivap  9044  divmul24ap  9048  divmuleqap  9049  recdivap  9050  divadddivap  9059  conjmulap  9061  prodgt0gt0  9183  ltmul12a  9192  lemul12b  9193  lediv2a  9227  qmulcl  10046  irrmul  10057  xrrege0  10237  ge0addcl  10393  ge0mulcl  10394  ge0xaddcl  10395  fzass4  10478  fzrev  10501  fzocatel  10627  expclzaplem  11013  expge0  11025  expge1  11026  lt2sq  11063  le2sq  11064  bernneq  11111  sq11ap  11158  ccatw2s1p1g  11427  ccatw2s1p2  11428  swrdccatin2  11515  sqrt11ap  11818  2clim  12083  climge0  12107  tanaddaplem  12521  opeo  12680  omeo  12681  cncongr1  12897  pcpremul  13092  pcmul  13100  ennnfonelemf1  13358  setscom  13441  dfgrp3mlem  13952  grplactcnv  13956  issubg4m  14045  resgrpisgrp  14047  ghmpreima  14118  ghmeql  14119  conjghm  14128  rngpropd  14303  lmodprop2d  14734  opnneissb  15305  cncnpi  15378  neitx  15418  txcnmpt  15423  txrest  15426  txdis1cn  15428  ptolemy  15975  cxplt3  16075  cxple3  16076  lgslem3  16219  lgsdir2  16250  lgsne0  16255  lgsquad3  16301  umgr2edg  16546  umgrvad2edg  16550  wlkeq  16693  clwwlkccatlem  16739