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  5400  foco  5601  fvco4  5749  fliftfun  5969  f1imaen2g  7033  fodju0  7438  mulcomnqg  7698  mulassnqg  7699  ltdcnq  7712  lt2addnq  7719  lt2mulnq  7720  enq0ref  7748  enq0tr  7749  addcmpblnq0  7758  nqpnq0nq  7768  nqnq0m  7770  mulcomnq0  7775  addlocpr  7851  nqprl  7866  nqpru  7867  prmuloc  7881  distrlem1prl  7897  distrlem1pru  7898  ltaddpr  7912  ltexprlemopu  7918  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemrl  7925  ltexprlemru  7927  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  caucvgprprlemopu  8014  addcomsrg  8070  mulcomsrg  8072  mulasssrg  8073  distrsrg  8074  addcnsr  8149  mulcnsr  8150  addcnsrec  8157  axaddcl  8179  axaddcom  8185  addsub4  8516  muladd  8657  mullt0  8754  apreim  8877  mulge0  8893  divmuldivap  8986  divmul24ap  8990  divmuleqap  8991  recdivap  8992  divadddivap  9001  conjmulap  9003  prodgt0gt0  9125  ltmul12a  9134  lemul12b  9135  lediv2a  9169  qmulcl  9969  irrmul  9979  xrrege0  10158  ge0addcl  10314  ge0mulcl  10315  ge0xaddcl  10316  fzass4  10396  fzrev  10418  fzocatel  10544  expclzaplem  10925  expge0  10937  expge1  10938  lt2sq  10975  le2sq  10976  bernneq  11022  sq11ap  11069  ccatw2s1p1g  11333  ccatw2s1p2  11334  swrdccatin2  11421  sqrt11ap  11723  2clim  11986  climge0  12010  tanaddaplem  12424  opeo  12583  omeo  12584  cncongr1  12800  pcpremul  12991  pcmul  12999  ennnfonelemf1  13169  setscom  13252  dfgrp3mlem  13811  grplactcnv  13815  issubg4m  13910  resgrpisgrp  13912  ghmpreima  13983  ghmeql  13984  conjghm  13993  rngpropd  14099  lmodprop2d  14496  opnneissb  15020  cncnpi  15093  neitx  15133  txcnmpt  15138  txrest  15141  txdis1cn  15143  ptolemy  15689  cxplt3  15785  cxple3  15786  lgslem3  15875  lgsdir2  15906  lgsne0  15911  lgsquad3  15957  umgr2edg  16202  umgrvad2edg  16206  wlkeq  16349  clwwlkccatlem  16395