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

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

Proof of Theorem 3adant3r1
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1257 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr1 1212 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  pltletr  16740  latjlej1  16834  latjlej2  16835  latnlej  16837  latnlej2  16840  latmlem2  16851  latledi  16858  latjass  16864  latj32  16866  latj13  16867  ipopos  16929  tsrlemax  16989  imasmnd2  17096  grpsubsub  17273  grpnnncan2  17281  imasgrp2  17299  mulgnn0ass  17347  mulgsubdir  17351  cmn32  17980  ablsubadd  17986  imasring  18388  zntoslem  19669  xmettri3  21909  mettri3  21910  xmetrtri  21911  xmetrtri2  21912  metrtri  21913  cphdivcl  22714  cphassr  22743  relogbmulexp  24233  grpodivdiv  26544  grpomuldivass  26545  grpopnpcan2  26548  grponnncan2  26549  ablo32  26556  ablodivdiv4  26561  ablodiv32  26562  ablonnncan  26563  nvmdi  26675  nvsubsub23  26687  nvmtri2  26705  dipdi  26888  dipassr  26891  dipsubdir  26893  dipsubdi  26894  dvrcan5  28930  cgr3tr4  31135  cgr3rflx  31137  endofsegid  31168  seglemin  31196  broutsideof2  31205  rngosubdi  32717  rngosubdir  32718  isdrngo2  32730  crngm23  32774  dmncan2  32849  latmassOLD  33337  latm32  33339  cvrnbtwn4  33387  cvrcmp2  33392  ltcvrntr  33531  atcvrj0  33535  3dim3  33576  paddasslem17  33943  paddass  33945  lautlt  34198  lautcvr  34199  lautj  34200  lautm  34201  erngdvlem3  35099  dvalveclem  35135  mendlmod  36585  upgr1wlkvtxedg  40855
  Copyright terms: Public domain W3C validator