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

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

Proof of Theorem 3adant3r2
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1257 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr2 1213 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  plttr  16739  latjlej2  16835  latmlem1  16850  latmlem2  16851  latledi  16858  latmlej11  16859  latmlej12  16860  ipopos  16929  grppnpcan2  17278  mulgsubdir  17351  imasring  18388  zntoslem  19669  mettri2  21897  mettri  21908  xmetrtri  21911  xmetrtri2  21912  metrtri  21913  grpopnpcan2  26548  grponnncan2  26549  ablomuldiv  26559  ablonnncan1  26565  nvmdi  26675  dipdi  26888  dipassr  26891  dipsubdir  26893  dipsubdi  26894  btwncomim  31096  cgr3tr4  31135  cgr3rflx  31137  colinbtwnle  31201  rngosubdi  32717  rngosubdir  32718  dmncan1  32848  dmncan2  32849  omlfh1N  33366  omlfh3N  33367  cvrnbtwn3  33384  cvrnbtwn4  33387  cvrcmp2  33392  hlatjrot  33480  cvrat3  33549  lplnribN  33658  ltrn2ateq  34288  dvalveclem  35135  mendlmod  36585
  Copyright terms: Public domain W3C validator