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

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

Proof of Theorem 3adant3r3
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1114 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1177 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  ressress  16140  plttr  17171  plelttr  17173  latledi  17290  latmlej11  17291  latmlej21  17293  latmlej22  17294  latjass  17296  latj12  17297  latj31  17300  ipopos  17361  latdisdlem  17390  imasmnd2  17528  imasmnd  17529  grpaddsubass  17706  grpsubsub4  17709  grpnpncan  17711  imasgrp2  17731  imasgrp  17732  frgp0  18373  cmn12  18413  abladdsub  18420  imasring  18819  dvrass  18890  lss1  19141  islmhm2  19240  psrgrp  19600  psrlmod  19603  zntoslem  20107  ipdir  20186  t1sep  21376  mettri2  22347  xmetrtri  22361  xmetrtri2  22362  pi1grplem  23049  dchrabl  25178  motgrp  25637  xmstrkgc  25965  ax5seglem4  26011  grpomuldivass  27704  ablomuldiv  27715  ablodivdiv4  27717  nvmdi  27812  dipdi  28007  dipsubdir  28012  dipsubdi  28013  cgr3tr4  32465  cgr3rflx  32467  seglemin  32526  linerflx1  32562  elicc3  32617  rngosubdi  34057  rngosubdir  34058  igenval2  34178  dmncan1  34188  latmassOLD  35019  omlfh1N  35048  omlfh3N  35049  cvrnbtwn  35061  cvrnbtwn2  35065  cvrnbtwn4  35069  hlatj12  35160  cvrntr  35214  islpln2a  35337  3atnelvolN  35375  elpadd2at2  35596  paddasslem17  35625  paddass  35627  paddssw2  35633  pmapjlln1  35644  ltrn2ateq  35970  cdlemc3  35983  cdleme1b  36016  cdleme3b  36019  cdleme3c  36020  cdleme9b  36042  erngdvlem3  36780  erngdvlem3-rN  36788  dvalveclem  36816  mendlmod  38265  lincsumscmcl  42732
  Copyright terms: Public domain W3C validator