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

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

Proof of Theorem 3adant3r1
StepHypRef Expression
1 ad4ant3.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213expb 1121 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr1 1170 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:  dif1en  9110  ccatswrd  14565  plttr  18239  pltletr  18240  latjlej1  18350  latjlej2  18351  latnlej  18353  latnlej2  18356  latmlem2  18367  latledi  18374  latjass  18380  latj32  18382  latj13  18383  ipopos  18433  tsrlemax  18483  imasmnd2  18601  grpsubsub  18844  grpnnncan2  18852  imasgrp2  18870  mulgnn0ass  18920  mulgsubdir  18924  cmn32  19590  ablsubadd  19598  imasring  20053  zntoslem  20986  xmettri3  23729  mettri3  23730  xmetrtri  23731  xmetrtri2  23732  metrtri  23733  cphdivcl  24569  cphassr  24599  relogbmulexp  26151  grpodivdiv  29531  grpomuldivass  29532  ablo32  29540  ablodivdiv4  29545  ablodiv32  29546  nvmdi  29639  dipdi  29834  dipassr  29837  dipsubdir  29839  dipsubdi  29840  dvrcan5  32127  cgr3tr4  34690  cgr3rflx  34692  endofsegid  34723  seglemin  34751  broutsideof2  34760  rngosubdi  36454  rngosubdir  36455  isdrngo2  36467  crngm23  36511  dmncan2  36586  latmassOLD  37741  latm32  37743  cvrnbtwn4  37791  cvrcmp2  37796  ltcvrntr  37937  atcvrj0  37941  3dim3  37982  paddasslem17  38349  paddass  38351  lautlt  38604  lautcvr  38605  lautj  38606  lautm  38607  erngdvlem3  39503  dvalveclem  39538  isdomn4  40674  mendlmod  41567
  Copyright terms: Public domain W3C validator