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

Theorem 3adant3r3 1183
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 1119 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr3 1170 1 ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 206  df-an 396  df-3an 1088
This theorem is referenced by:  infsupprpr  9503  ressress  17198  plttr  18300  plelttr  18302  latledi  18435  latmlej11  18436  latmlej21  18438  latmlej22  18439  latjass  18441  latj12  18442  latj31  18445  latdisdlem  18454  ipopos  18494  imasmnd2  18697  imasmnd  18698  grpaddsubass  18950  grpsubsub4  18953  grpnpncan  18955  imasgrp2  18975  imasgrp  18976  frgp0  19670  cmn12  19712  abladdsub  19722  imasrng  20072  imasring  20219  dvrass  20300  lss1  20694  islmhm2  20794  isdomn4  21119  zntoslem  21332  ipdir  21412  psrgrpOLD  21738  psrlmod  21741  t1sep  23095  mettri2  24068  xmetrtri  24082  xmetrtri2  24083  pi1grplem  24797  dchrabl  26994  motgrp  28062  xmstrkgc  28411  ax5seglem4  28458  grpomuldivass  30062  ablomuldiv  30073  ablodivdiv4  30075  nvmdi  30169  dipdi  30364  dipsubdir  30369  dipsubdi  30370  cgr3tr4  35329  cgr3rflx  35331  seglemin  35390  linerflx1  35426  elicc3  35506  rngosubdi  37117  rngosubdir  37118  igenval2  37238  dmncan1  37248  latmassOLD  38403  omlfh1N  38432  omlfh3N  38433  cvrnbtwn  38445  cvrnbtwn2  38449  cvrnbtwn4  38453  hlatj12  38545  cvrntr  38600  islpln2a  38723  3atnelvolN  38761  elpadd2at2  38982  paddasslem17  39011  paddass  39013  paddssw2  39019  pmapjlln1  39030  ltrn2ateq  39355  cdlemc3  39368  cdleme1b  39401  cdleme3b  39404  cdleme3c  39405  cdleme9b  39427  erngdvlem3  40165  erngdvlem3-rN  40173  dvalveclem  40200  mendlmod  42238  lincsumscmcl  47202
  Copyright terms: Public domain W3C validator