MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2ant2r Structured version   Visualization version   GIF version

Theorem ad2ant2r 743
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
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrr 713 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantlr 711 1 (((𝜑𝜃) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  disjxiun  5059  fundif  6399  funcnvqp  6414  foco  6598  fliftfun  7060  wfr3g  7947  omordi  8185  f1imaen2g  8562  isinf  8723  frfi  8755  acndom2  9472  infxp  9629  cff1  9672  isf32lem7  9773  fpwwe2lem12  10055  inawinalem  10103  inar1  10189  grur1  10234  genpnnp  10419  ltexprlem7  10456  prlem936  10461  reclem3pr  10463  1re  10633  addsub4  10921  muladd  11064  lt2add  11117  mullt0  11151  mulnzcnopr  11278  divmuldiv  11332  divmul24  11336  divmuleq  11337  recdiv  11338  divadddiv  11347  conjmul  11349  prodgt0  11479  ltmul12a  11488  lemul12b  11489  lediv12a  11525  lediv2a  11526  qmulcl  12359  irrmul  12366  xrrege0  12560  xmulge0  12670  ge0addcl  12841  ge0mulcl  12842  ge0xaddcl  12843  ge0xmulcl  12844  fzass4  12938  fzrev  12963  fzocatel  13094  serge0  13417  expclzlem  13446  expge0  13458  expge1  13459  lt2sq  13491  le2sq  13492  bernneq  13583  ccatw2s1p1OLD  13989  ccatw2s1p2  13990  swrdccatin2  14084  cshwleneq  14172  s2eq2seq  14292  wwlktovf1  14314  sqrmo  14604  limsupval2  14830  o1lo12  14888  climrlim2  14897  2clim  14922  climsup  15019  tanaddlem  15511  opeo  15706  omeo  15707  divalglem8  15743  coprmproddvdslem  15998  pcpremul  16172  pcmul  16180  setscom  16519  fpwipodrs  17766  gsumsgrpccat  17989  dfgrp3lem  18129  grplactcnv  18134  resgrpisgrp  18232  ghmpreima  18312  ghmeql  18313  conjghm  18321  pgpfi  18652  lmodprop2d  19618  lidlmcl  19911  xrs1mnd  20499  absabv  20518  frlmipval  20839  lmimco  20904  mavmulass  21074  mdetdiaglem  21123  cramerimplem2  21209  opnneissb  21638  cncnpi  21802  pnrmopn  21867  cmpsub  21924  connsub  21945  t1connperf  21960  neitx  22131  txcnmpt  22148  txrest  22155  txdis1cn  22159  tx1stc  22174  qtopcn  22238  trfg  22415  rnelfmlem  22476  flffbas  22519  nmo0  23259  nmoid  23266  cfilfcls  23792  iscmet3lem2  23810  caubl  23826  relcmpcmet  23836  ovolun  24015  ovolicc2lem3  24035  volsup  24072  ioombl1lem4  24077  ismbf3d  24170  mbfimaopnlem  24171  i1faddlem  24209  itgle  24325  ellimc2  24390  ftc1a  24549  dgrmul  24775  itgulm  24911  abelthlem8  24942  ptolemy  24997  logdivlt  25117  cxplt3  25196  cxple3  25197  o1cxp  25466  basellem4  25575  sqf11  25630  lgslem3  25789  lgsdir2  25820  lgsne0  25825  lgsquad3  25877  chpo1ubb  25971  vmadivsumb  25973  rpvmasumlem  25977  dchrisum0re  26003  dchrisum0  26010  selberg2b  26042  selberg3lem2  26048  pntrsumbnd  26056  pntrlog2bnd  26074  ishpg  26459  axcontlem2  26665  umgr2edg  26905  umgrvad2edg  26909  uhgrspan1  26999  wlkeq  27329  clwwlkccatlem  27681  wwlksext2clwwlk  27750  conngrv2edg  27888  frgrnbnb  27986  frgrwopreglem5lem  28013  frgrwopreglem5ALT  28015  grporcan  28209  blocni  28496  ubthlem3  28563  htthlem  28608  hvsub4  28728  shscli  29008  elspansn4  29264  5oalem2  29346  hosub4  29504  hmops  29711  hmopco  29714  adjadd  29784  hstpyth  29920  hstles  29922  mdsl0  30001  mdslmd1lem2  30017  chirredlem1  30081  chirredlem2  30082  chirredlem3  30083  chirredlem4  30084  mdsymlem6  30099  cdj3lem2b  30128  1stpreimas  30354  mdetpmtr2  30975  esumpcvgval  31223  signstfvc  31730  satffunlem  32532  frr3g  33005  nocvxmin  33132  tailfb  33609  isbasisrelowllem1  34505  isbasisrelowllem2  34506  poimirlem14  34773  heicant  34794  mblfinlem4  34799  ismblfin  34800  itg2addnc  34813  ftc1cnnc  34833  filbcmb  34883  prdsbnd  34939  ismtyval  34946  heiborlem8  34964  ghomco  35037  mzpindd  39204  mulltgt0  41140  stoweidlem46  42193  fourierdlem73  42326  iccelpart  43421  bgoldbtbnd  43802  2zrngmmgm  44045  srhmsubc  44175  srhmsubcALTV  44193  zlmodzxzsubm  44235  zlmodzxzsub  44236
  Copyright terms: Public domain W3C validator