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  5066  fundif  6406  funcnvqp  6421  foco  6605  fliftfun  7068  wfr3g  7956  omordi  8195  f1imaen2g  8573  isinf  8734  frfi  8766  acndom2  9483  infxp  9640  cff1  9683  isf32lem7  9784  fpwwe2lem12  10066  inawinalem  10114  inar1  10200  grur1  10245  genpnnp  10430  ltexprlem7  10467  prlem936  10472  reclem3pr  10474  1re  10644  addsub4  10932  muladd  11075  lt2add  11128  mullt0  11162  mulnzcnopr  11289  divmuldiv  11343  divmul24  11347  divmuleq  11348  recdiv  11349  divadddiv  11358  conjmul  11360  prodgt0  11490  ltmul12a  11499  lemul12b  11500  lediv12a  11536  lediv2a  11537  qmulcl  12369  irrmul  12376  xrrege0  12570  xmulge0  12680  ge0addcl  12851  ge0mulcl  12852  ge0xaddcl  12853  ge0xmulcl  12854  fzass4  12948  fzrev  12973  fzocatel  13104  serge0  13427  expclzlem  13456  expge0  13468  expge1  13469  lt2sq  13501  le2sq  13502  bernneq  13593  ccatw2s1p1OLD  13999  ccatw2s1p2  14000  swrdccatin2  14094  cshwleneq  14182  s2eq2seq  14302  wwlktovf1  14324  sqrmo  14614  limsupval2  14840  o1lo12  14898  climrlim2  14907  2clim  14932  climsup  15029  tanaddlem  15522  opeo  15717  omeo  15718  divalglem8  15754  coprmproddvdslem  16009  pcpremul  16183  pcmul  16191  setscom  16530  fpwipodrs  17777  gsumsgrpccat  18007  dfgrp3lem  18200  grplactcnv  18205  resgrpisgrp  18303  ghmpreima  18383  ghmeql  18384  conjghm  18392  pgpfi  18733  lmodprop2d  19699  lidlmcl  19993  xrs1mnd  20586  absabv  20605  frlmipval  20926  lmimco  20991  mavmulass  21161  mdetdiaglem  21210  cramerimplem2  21296  opnneissb  21725  cncnpi  21889  pnrmopn  21954  cmpsub  22011  connsub  22032  t1connperf  22047  neitx  22218  txcnmpt  22235  txrest  22242  txdis1cn  22246  tx1stc  22261  qtopcn  22325  trfg  22502  rnelfmlem  22563  flffbas  22606  nmo0  23347  nmoid  23354  cfilfcls  23880  iscmet3lem2  23898  caubl  23914  relcmpcmet  23924  ovolun  24103  ovolicc2lem3  24123  volsup  24160  ioombl1lem4  24165  ismbf3d  24258  mbfimaopnlem  24259  i1faddlem  24297  itgle  24413  ellimc2  24478  ftc1a  24637  dgrmul  24863  itgulm  24999  abelthlem8  25030  ptolemy  25085  logdivlt  25207  cxplt3  25286  cxple3  25287  o1cxp  25555  basellem4  25664  sqf11  25719  lgslem3  25878  lgsdir2  25909  lgsne0  25914  lgsquad3  25966  chpo1ubb  26060  vmadivsumb  26062  rpvmasumlem  26066  dchrisum0re  26092  dchrisum0  26099  selberg2b  26131  selberg3lem2  26137  pntrsumbnd  26145  pntrlog2bnd  26163  ishpg  26548  axcontlem2  26754  umgr2edg  26994  umgrvad2edg  26998  uhgrspan1  27088  wlkeq  27418  clwwlkccatlem  27770  wwlksext2clwwlk  27839  conngrv2edg  27977  frgrnbnb  28075  frgrwopreglem5lem  28102  frgrwopreglem5ALT  28104  grporcan  28298  blocni  28585  ubthlem3  28652  htthlem  28697  hvsub4  28817  shscli  29097  elspansn4  29353  5oalem2  29435  hosub4  29593  hmops  29800  hmopco  29803  adjadd  29873  hstpyth  30009  hstles  30011  mdsl0  30090  mdslmd1lem2  30106  chirredlem1  30170  chirredlem2  30171  chirredlem3  30172  chirredlem4  30173  mdsymlem6  30188  cdj3lem2b  30217  1stpreimas  30444  mdetpmtr2  31093  esumpcvgval  31341  signstfvc  31848  satffunlem  32652  frr3g  33125  nocvxmin  33252  tailfb  33729  isbasisrelowllem1  34640  isbasisrelowllem2  34641  poimirlem14  34910  heicant  34931  mblfinlem4  34936  ismblfin  34937  itg2addnc  34950  ftc1cnnc  34970  filbcmb  35019  prdsbnd  35075  ismtyval  35082  heiborlem8  35100  ghomco  35173  mzpindd  39349  mulltgt0  41285  stoweidlem46  42338  fourierdlem73  42471  iccelpart  43600  bgoldbtbnd  43981  2zrngmmgm  44224  srhmsubc  44354  srhmsubcALTV  44372  zlmodzxzsubm  44414  zlmodzxzsub  44415