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:  foco  5494  fvco4  5636  fliftfun  5846  f1imaen2g  6861  fodju0  7222  mulcomnqg  7469  mulassnqg  7470  ltdcnq  7483  lt2addnq  7490  lt2mulnq  7491  enq0ref  7519  enq0tr  7520  addcmpblnq0  7529  nqpnq0nq  7539  nqnq0m  7541  mulcomnq0  7546  addlocpr  7622  nqprl  7637  nqpru  7638  prmuloc  7652  distrlem1prl  7668  distrlem1pru  7669  ltaddpr  7683  ltexprlemopu  7689  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  caucvgprprlemopu  7785  addcomsrg  7841  mulcomsrg  7843  mulasssrg  7844  distrsrg  7845  addcnsr  7920  mulcnsr  7921  addcnsrec  7928  axaddcl  7950  axaddcom  7956  addsub4  8288  muladd  8429  mullt0  8526  apreim  8649  mulge0  8665  divmuldivap  8758  divmul24ap  8762  divmuleqap  8763  recdivap  8764  divadddivap  8773  conjmulap  8775  prodgt0gt0  8897  ltmul12a  8906  lemul12b  8907  lediv2a  8941  qmulcl  9730  irrmul  9740  xrrege0  9919  ge0addcl  10075  ge0mulcl  10076  ge0xaddcl  10077  fzass4  10156  fzrev  10178  fzocatel  10294  expclzaplem  10674  expge0  10686  expge1  10687  lt2sq  10724  le2sq  10725  bernneq  10771  sq11ap  10818  sqrt11ap  11222  2clim  11485  climge0  11509  tanaddaplem  11922  opeo  12081  omeo  12082  cncongr1  12298  pcpremul  12489  pcmul  12497  ennnfonelemf1  12662  setscom  12745  dfgrp3mlem  13302  grplactcnv  13306  issubg4m  13401  resgrpisgrp  13403  ghmpreima  13474  ghmeql  13475  conjghm  13484  rngpropd  13589  lmodprop2d  13982  opnneissb  14499  cncnpi  14572  neitx  14612  txcnmpt  14617  txrest  14620  txdis1cn  14622  ptolemy  15168  cxplt3  15264  cxple3  15265  lgslem3  15351  lgsdir2  15382  lgsne0  15387  lgsquad3  15433