Theorem ad2ant2r 753

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  disjxiun  5069  fundif  6534  funcnvqp  6549  fliftfun  7256  wfr3g  8259  omordi  8491  nadd4  8624  naddel12  8626  f1imaen2g  8952  isinf  9165  frfi  9185  frr3g  9671  acndom2  9967  infxp  10127  cff1  10171  isf32lem7  10272  fpwwe2lem11  10555  inawinalem  10603  inar1  10689  grur1  10734  genpnnp  10919  ltexprlem7  10956  prlem936  10961  reclem3pr  10963  1re  11135  addsub4  11428  muladd  11573  lt2add  11626  mullt0  11660  mulnzcnf  11787  divmuldiv  11846  divmul24  11850  divmuleq  11851  recdiv  11852  divadddiv  11861  conjmul  11863  prodgt0  11993  ltmul12a  12002  lemul12b  12003  lediv12a  12040  lediv2a  12041  qmulcl  12908  irrmul  12915  xrrege0  13117  xmulge0  13227  ge0addcl  13404  ge0mulcl  13405  ge0xaddcl  13406  ge0xmulcl  13407  fzass4  13507  fzrev  13532  fzocatel  13675  serge0  14009  expclzlem  14036  expge0  14051  expge1  14052  lt2sq  14086  le2sq  14087  bernneq  14182  ccatw2s1p2  14591  swrdccatin2  14682  cshwleneq  14770  s2eq2seq  14890  wwlktovf1  14910  sqrmo  15204  limsupval2  15433  o1lo12  15491  climrlim2  15500  2clim  15525  climsup  15623  tanaddlem  16124  opeo  16325  omeo  16326  divalglem8  16360  coprmproddvdslem  16622  pcpremul  16805  pcmul  16813  setscom  17141  fpwipodrs  18497  gsumsgrpccat  18799  dfgrp3lem  19005  grplactcnv  19010  resgrpisgrp  19114  ghmpreima  19204  ghmeql  19205  conjghm  19215  pgpfi  19571  rngpropd  20146  srhmsubc  20652  lmodprop2d  20914  cndrng  21376  absabv  21399  xrs1mnd  21415  frlmipval  21754  lmimco  21819  mavmulass  22532  mdetdiaglem  22581  cramerimplem2  22667  opnneissb  23097  cncnpi  23261  pnrmopn  23326  cmpsub  23383  connsub  23404  t1connperf  23419  neitx  23590  txcnmpt  23607  txrest  23614  txdis1cn  23618  tx1stc  23633  qtopcn  23697  trfg  23874  rnelfmlem  23935  flffbas  23978  nmo0  24718  nmoid  24725  cfilfcls  25259  iscmet3lem2  25277  caubl  25293  relcmpcmet  25303  ovolun  25484  ovolicc2lem3  25504  volsup  25541  ioombl1lem4  25546  ismbf3d  25639  mbfimaopnlem  25640  i1faddlem  25678  itgle  25795  ellimc2  25862  ftc1a  26022  dgrmul  26253  itgulm  26391  abelthlem8  26422  ptolemy  26478  logdivlt  26603  cxplt3  26682  cxple3  26683  o1cxp  26956  basellem4  27065  sqf11  27120  lgslem3  27280  lgsdir2  27311  lgsne0  27316  lgsquad3  27368  chpo1ubb  27462  vmadivsumb  27464  rpvmasumlem  27468  dchrisum0re  27494  dchrisum0  27501  selberg2b  27533  selberg3lem2  27539  pntrsumbnd  27547  pntrlog2bnd  27565  nocvxmin  27765  mulsgt0  28154  nnaddscl  28356  nnmulscl  28357  ishpg  28845  axcontlem2  29052  umgr2edg  29296  umgrvad2edg  29300  uhgrspan1  29390  wlkeq  29720  clwwlkccatlem  30077  wwlksext2clwwlk  30145  conngrv2edg  30283  frgrnbnb  30381  frgrwopreglem5lem  30408  frgrwopreglem5ALT  30410  grporcan  30607  blocni  30894  ubthlem3  30961  htthlem  31006  hvsub4  31126  shscli  31406  elspansn4  31662  5oalem2  31744  hosub4  31902  hmops  32109  hmopco  32112  adjadd  32182  hstpyth  32318  hstles  32320  mdsl0  32399  mdslmd1lem2  32415  chirredlem1  32479  chirredlem2  32480  chirredlem3  32481  chirredlem4  32482  mdsymlem6  32497  cdj3lem2b  32526  1stpreimas  32798  irngnzply1  33875  mdetpmtr2  34008  esumpcvgval  34262  signstfvc  34758  noinfepfnregs  35313  satffunlem  35629  mpomulnzcnf  36527  tailfb  36605  isbasisrelowllem1  37717  isbasisrelowllem2  37718  poimirlem14  38001  heicant  38022  mblfinlem4  38027  ismblfin  38028  itg2addnc  38041  ftc1cnnc  38059  filbcmb  38107  prdsbnd  38160  ismtyval  38167  heiborlem8  38185  ghomco  38258  mzpindd  43195  tfsconcatun  43782  oaun3lem1  43819  oaun3lem2  43820  mulltgt0  45470  stoweidlem46  46489  fourierdlem73  46622  cfsetsnfsetf1  47522  iccelpart  47908  bgoldbtbnd  48300  grimco  48380  isubgrgrim  48420  usgrgrtrirex  48441  grlictr  48506  2zrngmmgm  48743  srhmsubcALTV  48816  zlmodzxzsubm  48850  zlmodzxzsub  48851