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 398

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 209  df-an 399

This theorem is referenced by:  disjxiun  5049  fundif  6389  funcnvqp  6404  foco  6588  fliftfun  7051  wfr3g  7939  omordi  8178  f1imaen2g  8556  isinf  8717  frfi  8749  acndom2  9466  infxp  9623  cff1  9666  isf32lem7  9767  fpwwe2lem12  10049  inawinalem  10097  inar1  10183  grur1  10228  genpnnp  10413  ltexprlem7  10450  prlem936  10455  reclem3pr  10457  1re  10627  addsub4  10915  muladd  11058  lt2add  11111  mullt0  11145  mulnzcnopr  11272  divmuldiv  11326  divmul24  11330  divmuleq  11331  recdiv  11332  divadddiv  11341  conjmul  11343  prodgt0  11473  ltmul12a  11482  lemul12b  11483  lediv12a  11519  lediv2a  11520  qmulcl  12353  irrmul  12360  xrrege0  12554  xmulge0  12664  ge0addcl  12835  ge0mulcl  12836  ge0xaddcl  12837  ge0xmulcl  12838  fzass4  12935  fzrev  12960  fzocatel  13091  serge0  13414  expclzlem  13443  expge0  13455  expge1  13456  lt2sq  13488  le2sq  13489  bernneq  13580  ccatw2s1p1OLD  13981  ccatw2s1p2  13982  swrdccatin2  14076  cshwleneq  14164  s2eq2seq  14284  wwlktovf1  14306  sqrmo  14596  limsupval2  14822  o1lo12  14880  climrlim2  14889  2clim  14914  climsup  15011  tanaddlem  15504  opeo  15699  omeo  15700  divalglem8  15734  coprmproddvdslem  15989  pcpremul  16163  pcmul  16171  setscom  16510  fpwipodrs  17757  gsumsgrpccat  17987  dfgrp3lem  18180  grplactcnv  18185  resgrpisgrp  18283  ghmpreima  18363  ghmeql  18364  conjghm  18372  pgpfi  18713  lmodprop2d  19679  lidlmcl  19973  xrs1mnd  20566  absabv  20585  frlmipval  20906  lmimco  20971  mavmulass  21141  mdetdiaglem  21190  cramerimplem2  21276  opnneissb  21705  cncnpi  21869  pnrmopn  21934  cmpsub  21991  connsub  22012  t1connperf  22027  neitx  22198  txcnmpt  22215  txrest  22222  txdis1cn  22226  tx1stc  22241  qtopcn  22305  trfg  22482  rnelfmlem  22543  flffbas  22586  nmo0  23327  nmoid  23334  cfilfcls  23860  iscmet3lem2  23878  caubl  23894  relcmpcmet  23904  ovolun  24083  ovolicc2lem3  24103  volsup  24140  ioombl1lem4  24145  ismbf3d  24238  mbfimaopnlem  24239  i1faddlem  24277  itgle  24393  ellimc2  24460  ftc1a  24619  dgrmul  24846  itgulm  24982  abelthlem8  25013  ptolemy  25068  logdivlt  25190  cxplt3  25269  cxple3  25270  o1cxp  25538  basellem4  25647  sqf11  25702  lgslem3  25861  lgsdir2  25892  lgsne0  25897  lgsquad3  25949  chpo1ubb  26043  vmadivsumb  26045  rpvmasumlem  26049  dchrisum0re  26075  dchrisum0  26082  selberg2b  26114  selberg3lem2  26120  pntrsumbnd  26128  pntrlog2bnd  26146  ishpg  26531  axcontlem2  26737  umgr2edg  26977  umgrvad2edg  26981  uhgrspan1  27071  wlkeq  27401  clwwlkccatlem  27752  wwlksext2clwwlk  27820  conngrv2edg  27958  frgrnbnb  28056  frgrwopreglem5lem  28083  frgrwopreglem5ALT  28085  grporcan  28279  blocni  28566  ubthlem3  28633  htthlem  28678  hvsub4  28798  shscli  29078  elspansn4  29334  5oalem2  29416  hosub4  29574  hmops  29781  hmopco  29784  adjadd  29854  hstpyth  29990  hstles  29992  mdsl0  30071  mdslmd1lem2  30087  chirredlem1  30151  chirredlem2  30152  chirredlem3  30153  chirredlem4  30154  mdsymlem6  30169  cdj3lem2b  30198  1stpreimas  30427  mdetpmtr2  31099  esumpcvgval  31344  signstfvc  31851  satffunlem  32655  frr3g  33128  nocvxmin  33255  tailfb  33732  isbasisrelowllem1  34652  isbasisrelowllem2  34653  poimirlem14  34940  heicant  34961  mblfinlem4  34966  ismblfin  34967  itg2addnc  34980  ftc1cnnc  34998  filbcmb  35047  prdsbnd  35103  ismtyval  35110  heiborlem8  35128  ghomco  35201  mzpindd  39435  mulltgt0  41369  stoweidlem46  42421  fourierdlem73  42554  iccelpart  43683  bgoldbtbnd  44059  2zrngmmgm  44302  srhmsubc  44432  srhmsubcALTV  44450  zlmodzxzsubm  44492  zlmodzxzsub  44493