Theorem ad2ant2r 748

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  disjxiun  5083  fundif  6542  funcnvqp  6557  fliftfun  7261  wfr3g  8263  omordi  8495  nadd4  8628  naddel12  8630  f1imaen2g  8956  isinf  9169  frfi  9189  frr3g  9674  acndom2  9970  infxp  10130  cff1  10174  isf32lem7  10275  fpwwe2lem11  10558  inawinalem  10606  inar1  10692  grur1  10737  genpnnp  10922  ltexprlem7  10959  prlem936  10964  reclem3pr  10966  1re  11138  addsub4  11431  muladd  11576  lt2add  11629  mullt0  11663  mulnzcnf  11790  divmuldiv  11849  divmul24  11853  divmuleq  11854  recdiv  11855  divadddiv  11864  conjmul  11866  prodgt0  11996  ltmul12a  12005  lemul12b  12006  lediv12a  12043  lediv2a  12044  qmulcl  12911  irrmul  12918  xrrege0  13120  xmulge0  13230  ge0addcl  13407  ge0mulcl  13408  ge0xaddcl  13409  ge0xmulcl  13410  fzass4  13510  fzrev  13535  fzocatel  13678  serge0  14012  expclzlem  14039  expge0  14054  expge1  14055  lt2sq  14089  le2sq  14090  bernneq  14185  ccatw2s1p2  14594  swrdccatin2  14685  cshwleneq  14773  s2eq2seq  14893  wwlktovf1  14913  sqrmo  15207  limsupval2  15436  o1lo12  15494  climrlim2  15503  2clim  15528  climsup  15626  tanaddlem  16127  opeo  16328  omeo  16329  divalglem8  16363  coprmproddvdslem  16625  pcpremul  16808  pcmul  16816  setscom  17144  fpwipodrs  18500  gsumsgrpccat  18802  dfgrp3lem  19008  grplactcnv  19013  resgrpisgrp  19117  ghmpreima  19207  ghmeql  19208  conjghm  19218  pgpfi  19574  rngpropd  20149  srhmsubc  20651  lmodprop2d  20913  cndrng  21391  absabv  21417  xrs1mnd  21433  frlmipval  21772  lmimco  21837  mavmulass  22527  mdetdiaglem  22576  cramerimplem2  22662  opnneissb  23092  cncnpi  23256  pnrmopn  23321  cmpsub  23378  connsub  23399  t1connperf  23414  neitx  23585  txcnmpt  23602  txrest  23609  txdis1cn  23613  tx1stc  23628  qtopcn  23692  trfg  23869  rnelfmlem  23930  flffbas  23973  nmo0  24713  nmoid  24720  cfilfcls  25254  iscmet3lem2  25272  caubl  25288  relcmpcmet  25298  ovolun  25479  ovolicc2lem3  25499  volsup  25536  ioombl1lem4  25541  ismbf3d  25634  mbfimaopnlem  25635  i1faddlem  25673  itgle  25790  ellimc2  25857  ftc1a  26017  dgrmul  26248  itgulm  26389  abelthlem8  26420  ptolemy  26476  logdivlt  26601  cxplt3  26680  cxple3  26681  o1cxp  26955  basellem4  27064  sqf11  27119  lgslem3  27279  lgsdir2  27310  lgsne0  27315  lgsquad3  27367  chpo1ubb  27461  vmadivsumb  27463  rpvmasumlem  27467  dchrisum0re  27493  dchrisum0  27500  selberg2b  27532  selberg3lem2  27538  pntrsumbnd  27546  pntrlog2bnd  27564  nocvxmin  27764  mulsgt0  28153  nnaddscl  28355  nnmulscl  28356  ishpg  28844  axcontlem2  29051  umgr2edg  29295  umgrvad2edg  29299  uhgrspan1  29389  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  32797  irngnzply1  33854  mdetpmtr2  33987  esumpcvgval  34241  signstfvc  34737  noinfepfnregs  35295  satffunlem  35602  mpomulnzcnf  36500  tailfb  36578  isbasisrelowllem1  37688  isbasisrelowllem2  37689  poimirlem14  37972  heicant  37993  mblfinlem4  37998  ismblfin  37999  itg2addnc  38012  ftc1cnnc  38030  filbcmb  38078  prdsbnd  38131  ismtyval  38138  heiborlem8  38156  ghomco  38229  mzpindd  43195  tfsconcatun  43786  oaun3lem1  43823  oaun3lem2  43824  mulltgt0  45474  stoweidlem46  46495  fourierdlem73  46628  cfsetsnfsetf1  47522  iccelpart  47908  bgoldbtbnd  48300  grimco  48380  isubgrgrim  48420  usgrgrtrirex  48441  grlictr  48506  2zrngmmgm  48743  srhmsubcALTV  48816  zlmodzxzsubm  48850  zlmodzxzsub  48851