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

Theorem 3adant3r3 1181
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 1117 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1168 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  infsupprpr  8956  ressress  16558  plttr  17576  plelttr  17578  latledi  17695  latmlej11  17696  latmlej21  17698  latmlej22  17699  latjass  17701  latj12  17702  latj31  17705  ipopos  17766  latdisdlem  17795  imasmnd2  17944  imasmnd  17945  grpaddsubass  18185  grpsubsub4  18188  grpnpncan  18190  imasgrp2  18210  imasgrp  18211  frgp0  18882  cmn12  18923  abladdsub  18932  imasring  19369  dvrass  19440  lss1  19707  islmhm2  19807  zntoslem  20252  ipdir  20332  psrgrp  20640  psrlmod  20643  t1sep  21979  mettri2  22952  xmetrtri  22966  xmetrtri2  22967  pi1grplem  23658  dchrabl  25842  motgrp  26341  xmstrkgc  26684  ax5seglem4  26730  grpomuldivass  28328  ablomuldiv  28339  ablodivdiv4  28341  nvmdi  28435  dipdi  28630  dipsubdir  28635  dipsubdi  28636  cgr3tr4  33627  cgr3rflx  33629  seglemin  33688  linerflx1  33724  elicc3  33779  rngosubdi  35382  rngosubdir  35383  igenval2  35503  dmncan1  35513  latmassOLD  36524  omlfh1N  36553  omlfh3N  36554  cvrnbtwn  36566  cvrnbtwn2  36570  cvrnbtwn4  36574  hlatj12  36666  cvrntr  36720  islpln2a  36843  3atnelvolN  36881  elpadd2at2  37102  paddasslem17  37131  paddass  37133  paddssw2  37139  pmapjlln1  37150  ltrn2ateq  37475  cdlemc3  37488  cdleme1b  37521  cdleme3b  37524  cdleme3c  37525  cdleme9b  37547  erngdvlem3  38285  erngdvlem3-rN  38293  dvalveclem  38320  mendlmod  40130  lincsumscmcl  44835
  Copyright terms: Public domain W3C validator