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

Theorem 3adant3r2 1181
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 1118 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1168 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085
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 1087
This theorem is referenced by:  plttr  18328  latjlej2  18440  latmlem1  18455  latmlem2  18456  latledi  18463  latmlej11  18464  latmlej12  18465  ipopos  18522  grppnpcan2  18984  mulgsubdir  19063  imasrng  20111  imasring  20260  isdomn4  21244  zntoslem  21484  mettri2  24241  mettri  24252  xmetrtri  24255  xmetrtri2  24256  metrtri  24257  ablomuldiv  30356  ablonnncan1  30361  nvmdi  30452  dipdi  30647  dipassr  30650  dipsubdir  30652  dipsubdi  30653  btwncomim  35604  cgr3tr4  35643  cgr3rflx  35645  colinbtwnle  35709  rngosubdi  37413  rngosubdir  37414  dmncan1  37544  dmncan2  37545  omlfh1N  38725  omlfh3N  38726  cvrnbtwn3  38743  cvrnbtwn4  38746  cvrcmp2  38751  hlatjrot  38840  cvrat3  38910  lplnribN  39019  ltrn2ateq  39648  dvalveclem  40493  mendlmod  42608
  Copyright terms: Public domain W3C validator