Theorem ad2ant2r 745

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 715	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 713	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 206  df-an 397

This theorem is referenced by:  disjxiun  5145  fundif  6597  funcnvqp  6612  fliftfun  7311  wfr3g  8309  omordi  8568  nadd4  8699  naddel12  8701  f1imaen2g  9013  isinf  9262  isinfOLD  9263  frfi  9290  frr3g  9753  acndom2  10051  infxp  10212  cff1  10255  isf32lem7  10356  fpwwe2lem11  10638  inawinalem  10686  inar1  10772  grur1  10817  genpnnp  11002  ltexprlem7  11039  prlem936  11044  reclem3pr  11046  1re  11216  addsub4  11505  muladd  11648  lt2add  11701  mullt0  11735  mulnzcnopr  11862  divmuldiv  11916  divmul24  11920  divmuleq  11921  recdiv  11922  divadddiv  11931  conjmul  11933  prodgt0  12063  ltmul12a  12072  lemul12b  12073  lediv12a  12109  lediv2a  12110  qmulcl  12953  irrmul  12960  xrrege0  13155  xmulge0  13265  ge0addcl  13439  ge0mulcl  13440  ge0xaddcl  13441  ge0xmulcl  13442  fzass4  13541  fzrev  13566  fzocatel  13698  serge0  14024  expclzlem  14051  expge0  14066  expge1  14067  lt2sq  14100  le2sq  14101  bernneq  14194  ccatw2s1p2  14589  swrdccatin2  14681  cshwleneq  14769  s2eq2seq  14890  wwlktovf1  14910  sqrmo  15200  limsupval2  15426  o1lo12  15484  climrlim2  15493  2clim  15518  climsup  15618  tanaddlem  16111  opeo  16310  omeo  16311  divalglem8  16345  coprmproddvdslem  16601  pcpremul  16778  pcmul  16786  setscom  17115  fpwipodrs  18495  gsumsgrpccat  18723  dfgrp3lem  18923  grplactcnv  18928  resgrpisgrp  19029  ghmpreima  19116  ghmeql  19117  conjghm  19125  pgpfi  19475  lmodprop2d  20539  lidlmcl  20846  xrs1mnd  20989  absabv  21008  frlmipval  21340  lmimco  21405  mavmulass  22058  mdetdiaglem  22107  cramerimplem2  22193  opnneissb  22625  cncnpi  22789  pnrmopn  22854  cmpsub  22911  connsub  22932  t1connperf  22947  neitx  23118  txcnmpt  23135  txrest  23142  txdis1cn  23146  tx1stc  23161  qtopcn  23225  trfg  23402  rnelfmlem  23463  flffbas  23506  nmo0  24259  nmoid  24266  cfilfcls  24798  iscmet3lem2  24816  caubl  24832  relcmpcmet  24842  ovolun  25023  ovolicc2lem3  25043  volsup  25080  ioombl1lem4  25085  ismbf3d  25178  mbfimaopnlem  25179  i1faddlem  25217  itgle  25334  ellimc2  25401  ftc1a  25561  dgrmul  25791  itgulm  25927  abelthlem8  25958  ptolemy  26013  logdivlt  26136  cxplt3  26215  cxple3  26216  o1cxp  26486  basellem4  26595  sqf11  26650  lgslem3  26809  lgsdir2  26840  lgsne0  26845  lgsquad3  26897  chpo1ubb  26991  vmadivsumb  26993  rpvmasumlem  26997  dchrisum0re  27023  dchrisum0  27030  selberg2b  27062  selberg3lem2  27068  pntrsumbnd  27076  pntrlog2bnd  27094  nocvxmin  27287  mulsgt0  27610  ishpg  28048  axcontlem2  28261  umgr2edg  28504  umgrvad2edg  28508  uhgrspan1  28598  wlkeq  28929  clwwlkccatlem  29280  wwlksext2clwwlk  29348  conngrv2edg  29486  frgrnbnb  29584  frgrwopreglem5lem  29611  frgrwopreglem5ALT  29613  grporcan  29809  blocni  30096  ubthlem3  30163  htthlem  30208  hvsub4  30328  shscli  30608  elspansn4  30864  5oalem2  30946  hosub4  31104  hmops  31311  hmopco  31314  adjadd  31384  hstpyth  31520  hstles  31522  mdsl0  31601  mdslmd1lem2  31617  chirredlem1  31681  chirredlem2  31682  chirredlem3  31683  chirredlem4  31684  mdsymlem6  31699  cdj3lem2b  31728  1stpreimas  31965  irngnzply1  32815  mdetpmtr2  32873  esumpcvgval  33145  signstfvc  33654  satffunlem  34461  tailfb  35348  isbasisrelowllem1  36322  isbasisrelowllem2  36323  poimirlem14  36588  heicant  36609  mblfinlem4  36614  ismblfin  36615  itg2addnc  36628  ftc1cnnc  36646  filbcmb  36694  prdsbnd  36747  ismtyval  36754  heiborlem8  36772  ghomco  36845  mzpindd  41566  tfsconcatun  42169  oaun3lem1  42206  oaun3lem2  42207  mulltgt0  43788  stoweidlem46  44841  fourierdlem73  44974  cfsetsnfsetf1  45848  iccelpart  46180  bgoldbtbnd  46556  rngpropd  46752  2zrngmmgm  46923  srhmsubc  47053  srhmsubcALTV  47071  zlmodzxzsubm  47114  zlmodzxzsub  47115