Theorem ad2ant2r 747

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 717	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 715	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  5116  fundif  6585  funcnvqp  6600  fliftfun  7305  wfr3g  8321  omordi  8578  nadd4  8710  naddel12  8712  f1imaen2g  9029  isinf  9268  isinfOLD  9269  frfi  9293  frr3g  9770  acndom2  10068  infxp  10228  cff1  10272  isf32lem7  10373  fpwwe2lem11  10655  inawinalem  10703  inar1  10789  grur1  10834  genpnnp  11019  ltexprlem7  11056  prlem936  11061  reclem3pr  11063  1re  11235  addsub4  11526  muladd  11669  lt2add  11722  mullt0  11756  mulnzcnf  11883  divmuldiv  11941  divmul24  11945  divmuleq  11946  recdiv  11947  divadddiv  11956  conjmul  11958  prodgt0  12088  ltmul12a  12097  lemul12b  12098  lediv12a  12135  lediv2a  12136  qmulcl  12983  irrmul  12990  xrrege0  13190  xmulge0  13300  ge0addcl  13477  ge0mulcl  13478  ge0xaddcl  13479  ge0xmulcl  13480  fzass4  13579  fzrev  13604  fzocatel  13745  serge0  14074  expclzlem  14101  expge0  14116  expge1  14117  lt2sq  14151  le2sq  14152  bernneq  14247  ccatw2s1p2  14655  swrdccatin2  14747  cshwleneq  14835  s2eq2seq  14956  wwlktovf1  14976  sqrmo  15270  limsupval2  15496  o1lo12  15554  climrlim2  15563  2clim  15588  climsup  15686  tanaddlem  16184  opeo  16384  omeo  16385  divalglem8  16419  coprmproddvdslem  16681  pcpremul  16863  pcmul  16871  setscom  17199  fpwipodrs  18550  gsumsgrpccat  18818  dfgrp3lem  19021  grplactcnv  19026  resgrpisgrp  19130  ghmpreima  19221  ghmeql  19222  conjghm  19232  pgpfi  19586  rngpropd  20134  srhmsubc  20640  lmodprop2d  20881  cndrng  21361  xrs1mnd  21372  absabv  21392  frlmipval  21739  lmimco  21804  mavmulass  22487  mdetdiaglem  22536  cramerimplem2  22622  opnneissb  23052  cncnpi  23216  pnrmopn  23281  cmpsub  23338  connsub  23359  t1connperf  23374  neitx  23545  txcnmpt  23562  txrest  23569  txdis1cn  23573  tx1stc  23588  qtopcn  23652  trfg  23829  rnelfmlem  23890  flffbas  23933  nmo0  24674  nmoid  24681  cfilfcls  25226  iscmet3lem2  25244  caubl  25260  relcmpcmet  25270  ovolun  25452  ovolicc2lem3  25472  volsup  25509  ioombl1lem4  25514  ismbf3d  25607  mbfimaopnlem  25608  i1faddlem  25646  itgle  25763  ellimc2  25830  ftc1a  25996  dgrmul  26228  itgulm  26369  abelthlem8  26401  ptolemy  26457  logdivlt  26582  cxplt3  26661  cxple3  26662  o1cxp  26937  basellem4  27046  sqf11  27101  lgslem3  27262  lgsdir2  27293  lgsne0  27298  lgsquad3  27350  chpo1ubb  27444  vmadivsumb  27446  rpvmasumlem  27450  dchrisum0re  27476  dchrisum0  27483  selberg2b  27515  selberg3lem2  27521  pntrsumbnd  27529  pntrlog2bnd  27547  nocvxmin  27742  mulsgt0  28099  nnaddscl  28290  nnmulscl  28291  ishpg  28738  axcontlem2  28944  umgr2edg  29188  umgrvad2edg  29192  uhgrspan1  29282  wlkeq  29614  clwwlkccatlem  29970  wwlksext2clwwlk  30038  conngrv2edg  30176  frgrnbnb  30274  frgrwopreglem5lem  30301  frgrwopreglem5ALT  30303  grporcan  30499  blocni  30786  ubthlem3  30853  htthlem  30898  hvsub4  31018  shscli  31298  elspansn4  31554  5oalem2  31636  hosub4  31794  hmops  32001  hmopco  32004  adjadd  32074  hstpyth  32210  hstles  32212  mdsl0  32291  mdslmd1lem2  32307  chirredlem1  32371  chirredlem2  32372  chirredlem3  32373  chirredlem4  32374  mdsymlem6  32389  cdj3lem2b  32418  1stpreimas  32683  irngnzply1  33732  mdetpmtr2  33855  esumpcvgval  34109  signstfvc  34606  satffunlem  35423  mpomulnzcnf  36317  tailfb  36395  isbasisrelowllem1  37373  isbasisrelowllem2  37374  poimirlem14  37658  heicant  37679  mblfinlem4  37684  ismblfin  37685  itg2addnc  37698  ftc1cnnc  37716  filbcmb  37764  prdsbnd  37817  ismtyval  37824  heiborlem8  37842  ghomco  37915  mzpindd  42769  tfsconcatun  43361  oaun3lem1  43398  oaun3lem2  43399  mulltgt0  45046  stoweidlem46  46075  fourierdlem73  46208  cfsetsnfsetf1  47088  iccelpart  47447  bgoldbtbnd  47823  grimco  47902  isubgrgrim  47942  usgrgrtrirex  47962  grlictr  48020  2zrngmmgm  48227  srhmsubcALTV  48300  zlmodzxzsubm  48334  zlmodzxzsub  48335