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 394

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 395

This theorem is referenced by:  disjxiun  5141  fundif  6598  funcnvqp  6613  fliftfun  7314  wfr3g  8327  omordi  8586  nadd4  8718  naddel12  8720  f1imaen2g  9036  isinf  9285  isinfOLD  9286  frfi  9313  frr3g  9790  acndom2  10088  infxp  10247  cff1  10290  isf32lem7  10391  fpwwe2lem11  10673  inawinalem  10721  inar1  10807  grur1  10852  genpnnp  11037  ltexprlem7  11074  prlem936  11079  reclem3pr  11081  1re  11253  addsub4  11542  muladd  11685  lt2add  11738  mullt0  11772  mulnzcnf  11899  divmuldiv  11957  divmul24  11961  divmuleq  11962  recdiv  11963  divadddiv  11972  conjmul  11974  prodgt0  12104  ltmul12a  12113  lemul12b  12114  lediv12a  12151  lediv2a  12152  qmulcl  12995  irrmul  13002  xrrege0  13199  xmulge0  13309  ge0addcl  13483  ge0mulcl  13484  ge0xaddcl  13485  ge0xmulcl  13486  fzass4  13585  fzrev  13610  fzocatel  13742  serge0  14068  expclzlem  14095  expge0  14110  expge1  14111  lt2sq  14144  le2sq  14145  bernneq  14239  ccatw2s1p2  14638  swrdccatin2  14730  cshwleneq  14818  s2eq2seq  14939  wwlktovf1  14959  sqrmo  15249  limsupval2  15475  o1lo12  15533  climrlim2  15542  2clim  15567  climsup  15667  tanaddlem  16161  opeo  16360  omeo  16361  divalglem8  16395  coprmproddvdslem  16656  pcpremul  16838  pcmul  16846  setscom  17175  fpwipodrs  18558  gsumsgrpccat  18823  dfgrp3lem  19026  grplactcnv  19031  resgrpisgrp  19135  ghmpreima  19226  ghmeql  19227  conjghm  19237  pgpfi  19597  rngpropd  20151  srhmsubc  20652  lmodprop2d  20894  cndrng  21384  xrs1mnd  21395  absabv  21415  frlmipval  21771  lmimco  21836  mavmulass  22537  mdetdiaglem  22586  cramerimplem2  22672  opnneissb  23104  cncnpi  23268  pnrmopn  23333  cmpsub  23390  connsub  23411  t1connperf  23426  neitx  23597  txcnmpt  23614  txrest  23621  txdis1cn  23625  tx1stc  23640  qtopcn  23704  trfg  23881  rnelfmlem  23942  flffbas  23985  nmo0  24738  nmoid  24745  cfilfcls  25288  iscmet3lem2  25306  caubl  25322  relcmpcmet  25332  ovolun  25514  ovolicc2lem3  25534  volsup  25571  ioombl1lem4  25576  ismbf3d  25669  mbfimaopnlem  25670  i1faddlem  25708  itgle  25825  ellimc2  25892  ftc1a  26058  dgrmul  26293  itgulm  26432  abelthlem8  26464  ptolemy  26519  logdivlt  26643  cxplt3  26722  cxple3  26723  o1cxp  26998  basellem4  27107  sqf11  27162  lgslem3  27323  lgsdir2  27354  lgsne0  27359  lgsquad3  27411  chpo1ubb  27505  vmadivsumb  27507  rpvmasumlem  27511  dchrisum0re  27537  dchrisum0  27544  selberg2b  27576  selberg3lem2  27582  pntrsumbnd  27590  pntrlog2bnd  27608  nocvxmin  27803  mulsgt0  28140  nnaddscl  28310  nnmulscl  28311  ishpg  28681  axcontlem2  28894  umgr2edg  29140  umgrvad2edg  29144  uhgrspan1  29234  wlkeq  29566  clwwlkccatlem  29917  wwlksext2clwwlk  29985  conngrv2edg  30123  frgrnbnb  30221  frgrwopreglem5lem  30248  frgrwopreglem5ALT  30250  grporcan  30446  blocni  30733  ubthlem3  30800  htthlem  30845  hvsub4  30965  shscli  31245  elspansn4  31501  5oalem2  31583  hosub4  31741  hmops  31948  hmopco  31951  adjadd  32021  hstpyth  32157  hstles  32159  mdsl0  32238  mdslmd1lem2  32254  chirredlem1  32318  chirredlem2  32319  chirredlem3  32320  chirredlem4  32321  mdsymlem6  32336  cdj3lem2b  32365  1stpreimas  32615  irngnzply1  33571  mdetpmtr2  33650  esumpcvgval  33922  signstfvc  34431  satffunlem  35240  mpomulnzcnf  36022  tailfb  36100  isbasisrelowllem1  37073  isbasisrelowllem2  37074  poimirlem14  37346  heicant  37367  mblfinlem4  37372  ismblfin  37373  itg2addnc  37386  ftc1cnnc  37404  filbcmb  37452  prdsbnd  37505  ismtyval  37512  heiborlem8  37530  ghomco  37603  mzpindd  42438  tfsconcatun  43038  oaun3lem1  43075  oaun3lem2  43076  mulltgt0  44656  stoweidlem46  45701  fourierdlem73  45834  cfsetsnfsetf1  46708  iccelpart  47039  bgoldbtbnd  47415  grimco  47493  gricer  47506  isubgrgrim  47510  grlictr  47539  2zrngmmgm  47663  srhmsubcALTV  47736  zlmodzxzsubm  47772  zlmodzxzsub  47773