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 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  plttr  18239  latjlej2  18351  latmlem1  18366  latmlem2  18367  latledi  18374  latmlej11  18375  latmlej12  18376  ipopos  18433  grppnpcan2  18849  mulgsubdir  18924  imasring  20053  zntoslem  20986  mettri2  23717  mettri  23728  xmetrtri  23731  xmetrtri2  23732  metrtri  23733  ablomuldiv  29543  ablonnncan1  29548  nvmdi  29639  dipdi  29834  dipassr  29837  dipsubdir  29839  dipsubdi  29840  btwncomim  34651  cgr3tr4  34690  cgr3rflx  34692  colinbtwnle  34756  rngosubdi  36454  rngosubdir  36455  dmncan1  36585  dmncan2  36586  omlfh1N  37770  omlfh3N  37771  cvrnbtwn3  37788  cvrnbtwn4  37791  cvrcmp2  37796  hlatjrot  37885  cvrat3  37955  lplnribN  38064  ltrn2ateq  38693  dvalveclem  39538  isdomn4  40674  mendlmod  41567
  Copyright terms: Public domain W3C validator