Theorem ad2ant2r 760

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5105  fundifOLD  6619  funcnvqp  6634  xpsntpg  7176  fliftfun  7351  wfr3g  8375  omordi  8612  nadd4  8746  naddel12  8748  f1imaen2g  9080  isinf  9294  frfi  9314  frr3g  9797  acndom2  10172  infxp  10331  cff1  10375  isf32lem7  10476  fpwwe2lem11  10765  inawinalem  10813  inar1  10899  grur1  10944  genpnnp  11129  ltexprlem7  11166  prlem936  11171  reclem3pr  11173  1re  11347  addsub4  11640  muladd  11787  lt2add  11841  mullt0  11875  mulnzcnf  12002  divmuldiv  12057  divmul24  12061  divmuleq  12062  recdiv  12063  divadddiv  12072  conjmul  12074  prodgt0  12204  ltmul12a  12213  lemul12b  12214  lediv12a  12250  lediv2a  12251  qmulcl  13135  irrmul  13142  xrrege0  13344  xmulge0  13454  ge0addcl  13631  ge0mulcl  13632  ge0xaddcl  13633  ge0xmulcl  13634  fzass4  13736  fzrev  13761  fzocatel  13904  serge0  14239  expclzlem  14266  expge0  14281  expge1  14282  lt2sq  14316  le2sq  14317  bernneq  14414  ccatw2s1p2  14827  swrdccatin2  14920  cshwleneq  15010  s2eq2seq  15131  wwlktovf1  15153  sqrmo  15461  limsupval2  15691  o1lo12  15749  climrlim2  15758  2clim  15783  climsup  15881  tanaddlem  16378  opeo  16579  omeo  16580  divalglem8  16614  coprmproddvdslem  16881  pcpremul  17065  pcmul  17073  setscom  17402  fpwipodrs  18764  gsumsgrpccat  19086  dfgrp3lem  19298  grplactcnv  19303  resgrpisgrp  19408  ghmpreima  19502  ghmeql  19503  conjghm  19513  pgpfi  19870  rngpropd  20447  srhmsubc  20983  lmodprop2d  21250  cndrng  21759  absabv  21784  xrs1mnd  21800  frlmipval  22140  lmimco  22205  mavmulass  22919  mdetdiaglem  22968  cramerimplem2  23057  opnneissb  23487  cncnpi  23651  pnrmopn  23716  cmpsub  23773  connsub  23794  t1connperf  23809  neitx  23981  txcnmpt  23998  txrest  24005  txdis1cn  24009  tx1stc  24024  qtopcn  24088  trfg  24265  rnelfmlem  24326  flffbas  24369  nmo0  25109  nmoid  25116  cfilfcls  25650  iscmet3lem2  25668  caubl  25684  relcmpcmet  25694  ovolun  25875  ovolicc2lem3  25895  volsup  25932  ioombl1lem4  25937  ismbf3d  26030  mbfimaopnlem  26031  i1faddlem  26069  itgle  26185  ellimc2  26252  ftc1a  26412  dgrmul  26644  itgulm  26792  abelthlem8  26823  ptolemy  26882  logdivlt  27006  cxplt3  27085  cxple3  27086  o1cxp  27359  basellem4  27468  sqf11  27523  lgslem3  27683  lgsdir2  27714  lgsne0  27719  lgsquad3  27771  chpo1ubb  27865  vmadivsumb  27867  rpvmasumlem  27871  dchrisum0re  27897  dchrisum0  27904  selberg2b  27936  selberg3lem2  27942  pntrsumbnd  27950  pntrlog2bnd  27968  nocvxmin  28198  mulsgt0  28587  nnaddscl  28789  nnmulscl  28790  ishpg  29294  axcontlem2  29600  umgr2edg  29847  umgrvad2edg  29851  uhgrspan1  29941  wlkeq  30271  clwwlkccatlem  30637  wwlksext2clwwlk  30705  conngrv2edg  30853  frgrnbnb  30951  frgrwopreglem5lem  30978  frgrwopreglem5ALT  30980  grporcan  31177  blocni  31464  ubthlem3  31531  htthlem  31576  hvsub4  31696  shscli  31976  elspansn4  32232  5oalem2  32314  hosub4  32472  hmops  32679  hmopco  32682  adjadd  32752  hstpyth  32888  hstles  32890  mdsl0  32969  mdslmd1lem2  32985  chirredlem1  33049  chirredlem2  33050  chirredlem3  33051  chirredlem4  33052  mdsymlem6  33067  cdj3lem2b  33096  1stpreimas  33396  irngnzply1  34434  mdetpmtr2  34567  esumpcvgval  34821  signstfvc  35314  noinfepfnregs  35941  satffunlem  36374  nmulprop  37154  nmulel1  37179  mpomulnzcnf  37303  tailfb  37380  isbasisrelowllem1  38546  isbasisrelowllem2  38547  poimirlem14  38820  heicant  38841  mblfinlem4  38846  ismblfin  38847  itg2addnc  38860  ftc1cnnc  38878  filbcmb  38940  prdsbnd  38993  ismtyval  39000  heiborlem8  39018  ghomco  39091  mzpindd  44023  tfsconcatun  44600  oaun3lem1  44637  oaun3lem2  44638  mulltgt0  46313  stoweidlem46  47329  fourierdlem73  47462  cfsetsnfsetf1  48402  iccelpart  48788  bgoldbtbnd  49180  grimco  49260  isubgrgrim  49300  usgrgrtrirex  49321  grlictr  49386  2zrngmmgm  49622  srhmsubcALTV  49695  lazcjcl  49741  zlmodzxzsubm  49802  zlmodzxzsub  49803