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

Theorem 3adant3r2 1227
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 1142 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1204 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  plttr  17175  latjlej2  17271  latmlem1  17286  latmlem2  17287  latledi  17294  latmlej11  17295  latmlej12  17296  ipopos  17365  grppnpcan2  17714  mulgsubdir  17784  imasring  18821  zntoslem  20112  mettri2  22359  mettri  22370  xmetrtri  22373  xmetrtri2  22374  metrtri  22375  ablomuldiv  27735  ablonnncan1  27740  nvmdi  27831  dipdi  28026  dipassr  28029  dipsubdir  28031  dipsubdi  28032  btwncomim  32441  cgr3tr4  32480  cgr3rflx  32482  colinbtwnle  32546  rngosubdi  34055  rngosubdir  34056  dmncan1  34186  dmncan2  34187  omlfh1N  35038  omlfh3N  35039  cvrnbtwn3  35056  cvrnbtwn4  35059  cvrcmp2  35064  hlatjrot  35153  cvrat3  35222  lplnribN  35331  ltrn2ateq  35961  dvalveclem  36806  mendlmod  38264
  Copyright terms: Public domain W3C validator