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  7467  mulassnqg  7468  ltdcnq  7481  lt2addnq  7488  lt2mulnq  7489  enq0ref  7517  enq0tr  7518  addcmpblnq0  7527  nqpnq0nq  7537  nqnq0m  7539  mulcomnq0  7544  addlocpr  7620  nqprl  7635  nqpru  7636  prmuloc  7650  distrlem1prl  7666  distrlem1pru  7667  ltaddpr  7681  ltexprlemopu  7687  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  caucvgprprlemopu  7783  addcomsrg  7839  mulcomsrg  7841  mulasssrg  7842  distrsrg  7843  addcnsr  7918  mulcnsr  7919  addcnsrec  7926  axaddcl  7948  axaddcom  7954  addsub4  8286  muladd  8427  mullt0  8524  apreim  8647  mulge0  8663  divmuldivap  8756  divmul24ap  8760  divmuleqap  8761  recdivap  8762  divadddivap  8771  conjmulap  8773  prodgt0gt0  8895  ltmul12a  8904  lemul12b  8905  lediv2a  8939  qmulcl  9728  irrmul  9738  xrrege0  9917  ge0addcl  10073  ge0mulcl  10074  ge0xaddcl  10075  fzass4  10154  fzrev  10176  fzocatel  10292  expclzaplem  10672  expge0  10684  expge1  10685  lt2sq  10722  le2sq  10723  bernneq  10769  sq11ap  10816  sqrt11ap  11220  2clim  11483  climge0  11507  tanaddaplem  11920  opeo  12079  omeo  12080  cncongr1  12296  pcpremul  12487  pcmul  12495  ennnfonelemf1  12660  setscom  12743  dfgrp3mlem  13300  grplactcnv  13304  issubg4m  13399  resgrpisgrp  13401  ghmpreima  13472  ghmeql  13473  conjghm  13482  rngpropd  13587  lmodprop2d  13980  opnneissb  14475  cncnpi  14548  neitx  14588  txcnmpt  14593  txrest  14596  txdis1cn  14598  ptolemy  15144  cxplt3  15240  cxple3  15241  lgslem3  15327  lgsdir2  15358  lgsne0  15363  lgsquad3  15409