Theorem ad2ant2r 747

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

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  disjxiun  5050  fundif  6429  funcnvqp  6444  fliftfun  7121  wfr3g  8053  omordi  8294  f1imaen2g  8689  isinf  8891  frfi  8916  frr3g  9372  acndom2  9668  infxp  9829  cff1  9872  isf32lem7  9973  fpwwe2lem11  10255  inawinalem  10303  inar1  10389  grur1  10434  genpnnp  10619  ltexprlem7  10656  prlem936  10661  reclem3pr  10663  1re  10833  addsub4  11121  muladd  11264  lt2add  11317  mullt0  11351  mulnzcnopr  11478  divmuldiv  11532  divmul24  11536  divmuleq  11537  recdiv  11538  divadddiv  11547  conjmul  11549  prodgt0  11679  ltmul12a  11688  lemul12b  11689  lediv12a  11725  lediv2a  11726  qmulcl  12563  irrmul  12570  xrrege0  12764  xmulge0  12874  ge0addcl  13048  ge0mulcl  13049  ge0xaddcl  13050  ge0xmulcl  13051  fzass4  13150  fzrev  13175  fzocatel  13306  serge0  13630  expclzlem  13659  expge0  13671  expge1  13672  lt2sq  13704  le2sq  13705  bernneq  13796  ccatw2s1p1OLD  14199  ccatw2s1p2  14200  swrdccatin2  14294  cshwleneq  14382  s2eq2seq  14502  wwlktovf1  14524  sqrmo  14815  limsupval2  15041  o1lo12  15099  climrlim2  15108  2clim  15133  climsup  15233  tanaddlem  15727  opeo  15926  omeo  15927  divalglem8  15961  coprmproddvdslem  16219  pcpremul  16396  pcmul  16404  setscom  16733  fpwipodrs  18046  gsumsgrpccat  18266  dfgrp3lem  18461  grplactcnv  18466  resgrpisgrp  18564  ghmpreima  18644  ghmeql  18645  conjghm  18653  pgpfi  18994  lmodprop2d  19961  lidlmcl  20255  xrs1mnd  20401  absabv  20420  frlmipval  20741  lmimco  20806  mavmulass  21446  mdetdiaglem  21495  cramerimplem2  21581  opnneissb  22011  cncnpi  22175  pnrmopn  22240  cmpsub  22297  connsub  22318  t1connperf  22333  neitx  22504  txcnmpt  22521  txrest  22528  txdis1cn  22532  tx1stc  22547  qtopcn  22611  trfg  22788  rnelfmlem  22849  flffbas  22892  nmo0  23633  nmoid  23640  cfilfcls  24171  iscmet3lem2  24189  caubl  24205  relcmpcmet  24215  ovolun  24396  ovolicc2lem3  24416  volsup  24453  ioombl1lem4  24458  ismbf3d  24551  mbfimaopnlem  24552  i1faddlem  24590  itgle  24707  ellimc2  24774  ftc1a  24934  dgrmul  25164  itgulm  25300  abelthlem8  25331  ptolemy  25386  logdivlt  25509  cxplt3  25588  cxple3  25589  o1cxp  25857  basellem4  25966  sqf11  26021  lgslem3  26180  lgsdir2  26211  lgsne0  26216  lgsquad3  26268  chpo1ubb  26362  vmadivsumb  26364  rpvmasumlem  26368  dchrisum0re  26394  dchrisum0  26401  selberg2b  26433  selberg3lem2  26439  pntrsumbnd  26447  pntrlog2bnd  26465  ishpg  26850  axcontlem2  27056  umgr2edg  27297  umgrvad2edg  27301  uhgrspan1  27391  wlkeq  27721  clwwlkccatlem  28072  wwlksext2clwwlk  28140  conngrv2edg  28278  frgrnbnb  28376  frgrwopreglem5lem  28403  frgrwopreglem5ALT  28405  grporcan  28599  blocni  28886  ubthlem3  28953  htthlem  28998  hvsub4  29118  shscli  29398  elspansn4  29654  5oalem2  29736  hosub4  29894  hmops  30101  hmopco  30104  adjadd  30174  hstpyth  30310  hstles  30312  mdsl0  30391  mdslmd1lem2  30407  chirredlem1  30471  chirredlem2  30472  chirredlem3  30473  chirredlem4  30474  mdsymlem6  30489  cdj3lem2b  30518  1stpreimas  30758  mdetpmtr2  31488  esumpcvgval  31758  signstfvc  32265  satffunlem  33076  nocvxmin  33710  tailfb  34303  isbasisrelowllem1  35263  isbasisrelowllem2  35264  poimirlem14  35528  heicant  35549  mblfinlem4  35554  ismblfin  35555  itg2addnc  35568  ftc1cnnc  35586  filbcmb  35635  prdsbnd  35688  ismtyval  35695  heiborlem8  35713  ghomco  35786  mzpindd  40271  mulltgt0  42238  stoweidlem46  43262  fourierdlem73  43395  cfsetsnfsetf1  44225  iccelpart  44558  bgoldbtbnd  44934  2zrngmmgm  45177  srhmsubc  45307  srhmsubcALTV  45325  zlmodzxzsubm  45368  zlmodzxzsub  45369