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

Theorem 3adant3r3 1267
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant3r3 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)

Proof of Theorem 3adant3r3
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1257 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1214 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  ressress  15711  plttr  16739  plelttr  16741  latledi  16858  latmlej11  16859  latmlej21  16861  latmlej22  16862  latjass  16864  latj12  16865  latj31  16868  ipopos  16929  latdisdlem  16958  imasmnd2  17096  imasmnd  17097  grpaddsubass  17274  grpsubsub4  17277  grpnpncan  17279  imasgrp2  17299  imasgrp  17300  frgp0  17942  cmn12  17982  abladdsub  17989  imasring  18388  dvrass  18459  lss1  18706  islmhm2  18805  psrgrp  19165  psrlmod  19168  zntoslem  19669  ipdir  19748  t1sep  20926  mettri2  21897  xmetrtri  21911  xmetrtri2  21912  pi1grplem  22588  dchrabl  24696  motgrp  25156  xmstrkgc  25484  ax5seglem4  25530  grpomuldivass  26545  grpopnpcan2  26548  grponpncan  26550  ablomuldiv  26559  ablodivdiv4  26561  nvadd12  26646  nvmdi  26675  nvsubadd  26680  nvmtri2  26705  dipdi  26888  dipsubdir  26893  dipsubdi  26894  cgr3tr4  31135  cgr3rflx  31137  seglemin  31196  linerflx1  31232  elicc3  31287  rngosubdi  32710  rngosubdir  32711  igenval2  32831  dmncan1  32841  latmassOLD  33330  omlfh1N  33359  omlfh3N  33360  cvrnbtwn  33372  cvrnbtwn2  33376  cvrnbtwn4  33380  hlatj12  33471  cvrntr  33525  islpln2a  33648  3atnelvolN  33686  elpadd2at2  33907  paddasslem17  33936  paddass  33938  paddssw2  33944  pmapjlln1  33955  ltrn2ateq  34281  cdlemc3  34294  cdleme1b  34327  cdleme3b  34330  cdleme3c  34331  cdleme9b  34353  erngdvlem3  35092  erngdvlem3-rN  35100  dvalveclem  35128  mendlmod  36578  lincsumscmcl  42011
  Copyright terms: Public domain W3C validator