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

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

Proof of Theorem 3adant3r2
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1121 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1171 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  plttr  18387  latjlej2  18499  latmlem1  18514  latmlem2  18515  latledi  18522  latmlej11  18523  latmlej12  18524  ipopos  18581  grppnpcan2  19052  mulgsubdir  19132  imasrng  20174  imasring  20327  isdomn4  20716  zntoslem  21575  mettri2  24351  mettri  24362  xmetrtri  24365  xmetrtri2  24366  metrtri  24367  ablomuldiv  30571  ablonnncan1  30576  nvmdi  30667  dipdi  30862  dipassr  30865  dipsubdir  30867  dipsubdi  30868  btwncomim  36014  cgr3tr4  36053  cgr3rflx  36055  colinbtwnle  36119  rngosubdi  37952  rngosubdir  37953  dmncan1  38083  dmncan2  38084  omlfh1N  39259  omlfh3N  39260  cvrnbtwn3  39277  cvrnbtwn4  39280  cvrcmp2  39285  hlatjrot  39374  cvrat3  39444  lplnribN  39553  ltrn2ateq  40182  dvalveclem  41027  mendlmod  43201
  Copyright terms: Public domain W3C validator