Theorem ad2ant2r 760

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5100  fundif  6589  funcnvqp  6604  xpsntpg  7144  fliftfun  7320  wfr3g  8337  omordi  8574  nadd4  8708  naddel12  8710  f1imaen2g  9042  isinf  9256  frfi  9276  frr3g  9760  acndom2  10133  infxp  10292  cff1  10336  isf32lem7  10437  fpwwe2lem11  10726  inawinalem  10774  inar1  10860  grur1  10905  genpnnp  11090  ltexprlem7  11127  prlem936  11132  reclem3pr  11134  1re  11308  addsub4  11601  muladd  11748  lt2add  11801  mullt0  11835  mulnzcnf  11962  divmuldiv  12017  divmul24  12021  divmuleq  12022  recdiv  12023  divadddiv  12032  conjmul  12034  prodgt0  12164  ltmul12a  12173  lemul12b  12174  lediv12a  12210  lediv2a  12211  qmulcl  13095  irrmul  13102  xrrege0  13304  xmulge0  13414  ge0addcl  13591  ge0mulcl  13592  ge0xaddcl  13593  ge0xmulcl  13594  fzass4  13696  fzrev  13721  fzocatel  13864  serge0  14199  expclzlem  14226  expge0  14241  expge1  14242  lt2sq  14276  le2sq  14277  bernneq  14373  ccatw2s1p2  14785  swrdccatin2  14878  cshwleneq  14968  s2eq2seq  15088  wwlktovf1  15110  sqrmo  15418  limsupval2  15647  o1lo12  15705  climrlim2  15714  2clim  15739  climsup  15837  tanaddlem  16334  opeo  16535  omeo  16536  divalglem8  16570  coprmproddvdslem  16837  pcpremul  17021  pcmul  17029  setscom  17358  fpwipodrs  18714  gsumsgrpccat  19036  dfgrp3lem  19248  grplactcnv  19253  resgrpisgrp  19358  ghmpreima  19452  ghmeql  19453  conjghm  19463  pgpfi  19819  rngpropd  20396  srhmsubc  20932  lmodprop2d  21199  cndrng  21707  absabv  21730  xrs1mnd  21746  frlmipval  22085  lmimco  22150  mavmulass  22864  mdetdiaglem  22913  cramerimplem2  23002  opnneissb  23432  cncnpi  23596  pnrmopn  23661  cmpsub  23718  connsub  23739  t1connperf  23754  neitx  23926  txcnmpt  23943  txrest  23950  txdis1cn  23954  tx1stc  23969  qtopcn  24033  trfg  24210  rnelfmlem  24271  flffbas  24314  nmo0  25054  nmoid  25061  cfilfcls  25595  iscmet3lem2  25613  caubl  25629  relcmpcmet  25639  ovolun  25820  ovolicc2lem3  25840  volsup  25877  ioombl1lem4  25882  ismbf3d  25975  mbfimaopnlem  25976  i1faddlem  26014  itgle  26130  ellimc2  26197  ftc1a  26357  dgrmul  26589  itgulm  26735  abelthlem8  26766  ptolemy  26825  logdivlt  26949  cxplt3  27028  cxple3  27029  o1cxp  27302  basellem4  27411  sqf11  27466  lgslem3  27626  lgsdir2  27657  lgsne0  27662  lgsquad3  27714  chpo1ubb  27808  vmadivsumb  27810  rpvmasumlem  27814  dchrisum0re  27840  dchrisum0  27847  selberg2b  27879  selberg3lem2  27885  pntrsumbnd  27893  pntrlog2bnd  27911  nocvxmin  28141  mulsgt0  28530  nnaddscl  28732  nnmulscl  28733  ishpg  29237  axcontlem2  29543  umgr2edg  29790  umgrvad2edg  29794  uhgrspan1  29884  wlkeq  30214  clwwlkccatlem  30580  wwlksext2clwwlk  30648  conngrv2edg  30796  frgrnbnb  30894  frgrwopreglem5lem  30921  frgrwopreglem5ALT  30923  grporcan  31120  blocni  31407  ubthlem3  31474  htthlem  31519  hvsub4  31639  shscli  31919  elspansn4  32175  5oalem2  32257  hosub4  32415  hmops  32622  hmopco  32625  adjadd  32695  hstpyth  32831  hstles  32833  mdsl0  32912  mdslmd1lem2  32928  chirredlem1  32992  chirredlem2  32993  chirredlem3  32994  chirredlem4  32995  mdsymlem6  33010  cdj3lem2b  33039  1stpreimas  33299  irngnzply1  34323  mdetpmtr2  34456  esumpcvgval  34710  signstfvc  35203  noinfepfnregs  35800  satffunlem  36166  nmulprop  36939  nmulel1  36964  mpomulnzcnf  37088  tailfb  37165  isbasisrelowllem1  38278  isbasisrelowllem2  38279  poimirlem14  38552  heicant  38573  mblfinlem4  38578  ismblfin  38579  itg2addnc  38592  ftc1cnnc  38610  filbcmb  38674  prdsbnd  38727  ismtyval  38734  heiborlem8  38752  ghomco  38825  mzpindd  43756  tfsconcatun  44338  oaun3lem1  44375  oaun3lem2  44376  mulltgt0  46038  stoweidlem46  47055  fourierdlem73  47188  cfsetsnfsetf1  48128  iccelpart  48514  bgoldbtbnd  48906  grimco  48986  isubgrgrim  49026  usgrgrtrirex  49047  grlictr  49112  2zrngmmgm  49348  srhmsubcALTV  49421  zlmodzxzsubm  49470  zlmodzxzsub  49471