Theorem ad2ant2r 759

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  disjxiun  5106  fundif  6585  funcnvqp  6600  fliftfun  7310  wfr3g  8312  omordi  8547  nadd4  8681  naddel12  8683  f1imaen2g  9008  isinf  9221  frfi  9241  frr3g  9724  acndom2  10034  infxp  10193  cff1  10237  isf32lem7  10338  fpwwe2lem11  10621  inawinalem  10669  inar1  10755  grur1  10800  genpnnp  10985  ltexprlem7  11022  prlem936  11027  reclem3pr  11029  1re  11203  addsub4  11496  muladd  11641  lt2add  11694  mullt0  11728  mulnzcnf  11855  divmuldiv  11910  divmul24  11914  divmuleq  11915  recdiv  11916  divadddiv  11925  conjmul  11927  prodgt0  12057  ltmul12a  12066  lemul12b  12067  lediv12a  12103  lediv2a  12104  qmulcl  12986  irrmul  12993  xrrege0  13195  xmulge0  13305  ge0addcl  13482  ge0mulcl  13483  ge0xaddcl  13484  ge0xmulcl  13485  fzass4  13586  fzrev  13611  fzocatel  13754  serge0  14088  expclzlem  14115  expge0  14130  expge1  14131  lt2sq  14165  le2sq  14166  bernneq  14261  ccatw2s1p2  14671  swrdccatin2  14762  cshwleneq  14850  s2eq2seq  14970  wwlktovf1  14990  sqrmo  15298  limsupval2  15527  o1lo12  15585  climrlim2  15594  2clim  15619  climsup  15717  tanaddlem  16217  opeo  16418  omeo  16419  divalglem8  16453  coprmproddvdslem  16715  pcpremul  16898  pcmul  16906  setscom  17235  fpwipodrs  18591  gsumsgrpccat  18894  dfgrp3lem  19099  grplactcnv  19104  resgrpisgrp  19209  ghmpreima  19303  ghmeql  19304  conjghm  19314  pgpfi  19670  rngpropd  20247  srhmsubc  20779  lmodprop2d  21045  cndrng  21551  absabv  21574  xrs1mnd  21590  frlmipval  21929  lmimco  21994  mavmulass  22706  mdetdiaglem  22755  cramerimplem2  22841  opnneissb  23271  cncnpi  23435  pnrmopn  23500  cmpsub  23557  connsub  23578  t1connperf  23593  neitx  23764  txcnmpt  23781  txrest  23788  txdis1cn  23792  tx1stc  23807  qtopcn  23871  trfg  24048  rnelfmlem  24109  flffbas  24152  nmo0  24892  nmoid  24899  cfilfcls  25433  iscmet3lem2  25451  caubl  25467  relcmpcmet  25477  ovolun  25658  ovolicc2lem3  25678  volsup  25715  ioombl1lem4  25720  ismbf3d  25813  mbfimaopnlem  25814  i1faddlem  25852  itgle  25969  ellimc2  26036  ftc1a  26196  dgrmul  26427  itgulm  26571  abelthlem8  26602  ptolemy  26661  logdivlt  26786  cxplt3  26865  cxple3  26866  o1cxp  27139  basellem4  27248  sqf11  27303  lgslem3  27463  lgsdir2  27494  lgsne0  27499  lgsquad3  27551  chpo1ubb  27645  vmadivsumb  27647  rpvmasumlem  27651  dchrisum0re  27677  dchrisum0  27684  selberg2b  27716  selberg3lem2  27722  pntrsumbnd  27730  pntrlog2bnd  27748  nocvxmin  27948  mulsgt0  28337  nnaddscl  28539  nnmulscl  28540  ishpg  29041  axcontlem2  29315  umgr2edg  29559  umgrvad2edg  29563  uhgrspan1  29653  wlkeq  29983  clwwlkccatlem  30340  wwlksext2clwwlk  30408  conngrv2edg  30546  frgrnbnb  30644  frgrwopreglem5lem  30671  frgrwopreglem5ALT  30673  grporcan  30870  blocni  31157  ubthlem3  31224  htthlem  31269  hvsub4  31389  shscli  31669  elspansn4  31925  5oalem2  32007  hosub4  32165  hmops  32372  hmopco  32375  adjadd  32445  hstpyth  32581  hstles  32583  mdsl0  32662  mdslmd1lem2  32678  chirredlem1  32742  chirredlem2  32743  chirredlem3  32744  chirredlem4  32745  mdsymlem6  32760  cdj3lem2b  32789  1stpreimas  33051  irngnzply1  34081  mdetpmtr2  34214  esumpcvgval  34468  signstfvc  34961  noinfepfnregs  35545  satffunlem  35893  nmulprop  36682  nmulel1  36692  mpomulnzcnf  36811  tailfb  36888  isbasisrelowllem1  38001  isbasisrelowllem2  38002  poimirlem14  38285  heicant  38306  mblfinlem4  38311  ismblfin  38312  itg2addnc  38325  ftc1cnnc  38343  filbcmb  38391  prdsbnd  38444  ismtyval  38451  heiborlem8  38469  ghomco  38542  mzpindd  43477  tfsconcatun  44064  oaun3lem1  44101  oaun3lem2  44102  mulltgt0  45742  stoweidlem46  46760  fourierdlem73  46893  cfsetsnfsetf1  47796  iccelpart  48182  bgoldbtbnd  48574  grimco  48654  isubgrgrim  48694  usgrgrtrirex  48715  grlictr  48780  2zrngmmgm  49017  srhmsubcALTV  49090  zlmodzxzsubm  49139  zlmodzxzsub  49140