Theorem ad2ant2r 744

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 714	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 712	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 206  df-an 396

This theorem is referenced by:  disjxiun  5145  fundif  6597  funcnvqp  6612  fliftfun  7312  wfr3g  8311  omordi  8570  nadd4  8701  naddel12  8703  f1imaen2g  9015  isinf  9264  isinfOLD  9265  frfi  9292  frr3g  9755  acndom2  10053  infxp  10214  cff1  10257  isf32lem7  10358  fpwwe2lem11  10640  inawinalem  10688  inar1  10774  grur1  10819  genpnnp  11004  ltexprlem7  11041  prlem936  11046  reclem3pr  11048  1re  11219  addsub4  11508  muladd  11651  lt2add  11704  mullt0  11738  mulnzcnopr  11865  divmuldiv  11919  divmul24  11923  divmuleq  11924  recdiv  11925  divadddiv  11934  conjmul  11936  prodgt0  12066  ltmul12a  12075  lemul12b  12076  lediv12a  12112  lediv2a  12113  qmulcl  12956  irrmul  12963  xrrege0  13158  xmulge0  13268  ge0addcl  13442  ge0mulcl  13443  ge0xaddcl  13444  ge0xmulcl  13445  fzass4  13544  fzrev  13569  fzocatel  13701  serge0  14027  expclzlem  14054  expge0  14069  expge1  14070  lt2sq  14103  le2sq  14104  bernneq  14197  ccatw2s1p2  14592  swrdccatin2  14684  cshwleneq  14772  s2eq2seq  14893  wwlktovf1  14913  sqrmo  15203  limsupval2  15429  o1lo12  15487  climrlim2  15496  2clim  15521  climsup  15621  tanaddlem  16114  opeo  16313  omeo  16314  divalglem8  16348  coprmproddvdslem  16604  pcpremul  16781  pcmul  16789  setscom  17118  fpwipodrs  18498  gsumsgrpccat  18758  dfgrp3lem  18958  grplactcnv  18963  resgrpisgrp  19064  ghmpreima  19153  ghmeql  19154  conjghm  19164  pgpfi  19515  rngpropd  20069  lmodprop2d  20679  xrs1mnd  21184  absabv  21203  frlmipval  21554  lmimco  21619  mavmulass  22272  mdetdiaglem  22321  cramerimplem2  22407  opnneissb  22839  cncnpi  23003  pnrmopn  23068  cmpsub  23125  connsub  23146  t1connperf  23161  neitx  23332  txcnmpt  23349  txrest  23356  txdis1cn  23360  tx1stc  23375  qtopcn  23439  trfg  23616  rnelfmlem  23677  flffbas  23720  nmo0  24473  nmoid  24480  cfilfcls  25023  iscmet3lem2  25041  caubl  25057  relcmpcmet  25067  ovolun  25249  ovolicc2lem3  25269  volsup  25306  ioombl1lem4  25311  ismbf3d  25404  mbfimaopnlem  25405  i1faddlem  25443  itgle  25560  ellimc2  25627  ftc1a  25790  dgrmul  26021  itgulm  26157  abelthlem8  26188  ptolemy  26243  logdivlt  26366  cxplt3  26445  cxple3  26446  o1cxp  26716  basellem4  26825  sqf11  26880  lgslem3  27039  lgsdir2  27070  lgsne0  27075  lgsquad3  27127  chpo1ubb  27221  vmadivsumb  27223  rpvmasumlem  27227  dchrisum0re  27253  dchrisum0  27260  selberg2b  27292  selberg3lem2  27298  pntrsumbnd  27306  pntrlog2bnd  27324  nocvxmin  27517  mulsgt0  27840  ishpg  28278  axcontlem2  28491  umgr2edg  28734  umgrvad2edg  28738  uhgrspan1  28828  wlkeq  29159  clwwlkccatlem  29510  wwlksext2clwwlk  29578  conngrv2edg  29716  frgrnbnb  29814  frgrwopreglem5lem  29841  frgrwopreglem5ALT  29843  grporcan  30039  blocni  30326  ubthlem3  30393  htthlem  30438  hvsub4  30558  shscli  30838  elspansn4  31094  5oalem2  31176  hosub4  31334  hmops  31541  hmopco  31544  adjadd  31614  hstpyth  31750  hstles  31752  mdsl0  31831  mdslmd1lem2  31847  chirredlem1  31911  chirredlem2  31912  chirredlem3  31913  chirredlem4  31914  mdsymlem6  31929  cdj3lem2b  31958  1stpreimas  32195  irngnzply1  33045  mdetpmtr2  33103  esumpcvgval  33375  signstfvc  33884  satffunlem  34691  tailfb  35566  isbasisrelowllem1  36540  isbasisrelowllem2  36541  poimirlem14  36806  heicant  36827  mblfinlem4  36832  ismblfin  36833  itg2addnc  36846  ftc1cnnc  36864  filbcmb  36912  prdsbnd  36965  ismtyval  36972  heiborlem8  36990  ghomco  37063  mzpindd  41787  tfsconcatun  42390  oaun3lem1  42427  oaun3lem2  42428  mulltgt0  44009  stoweidlem46  45061  fourierdlem73  45194  cfsetsnfsetf1  46068  iccelpart  46400  bgoldbtbnd  46776  2zrngmmgm  46933  srhmsubc  47063  srhmsubcALTV  47081  zlmodzxzsubm  47124  zlmodzxzsub  47125