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

Theorem 3adant3r1 1272
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 1264 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr1 1218 1 ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  plttr  16951  pltletr  16952  latjlej1  17046  latjlej2  17047  latnlej  17049  latnlej2  17052  latmlem2  17063  latledi  17070  latjass  17076  latj32  17078  latj13  17079  ipopos  17141  tsrlemax  17201  imasmnd2  17308  grpsubsub  17485  grpnnncan2  17493  imasgrp2  17511  mulgnn0ass  17559  mulgsubdir  17563  cmn32  18192  ablsubadd  18198  imasring  18600  zntoslem  19886  xmettri3  22139  mettri3  22140  xmetrtri  22141  xmetrtri2  22142  metrtri  22143  cphdivcl  22963  cphassr  22993  relogbmulexp  24497  grpodivdiv  27364  grpomuldivass  27365  ablo32  27373  ablodivdiv4  27378  ablodiv32  27379  ablonnncan  27380  nvmdi  27473  dipdi  27668  dipassr  27671  dipsubdir  27673  dipsubdi  27674  dvrcan5  29767  cgr3tr4  32134  cgr3rflx  32136  endofsegid  32167  seglemin  32195  broutsideof2  32204  rngosubdi  33715  rngosubdir  33716  isdrngo2  33728  crngm23  33772  dmncan2  33847  latmassOLD  34335  latm32  34337  cvrnbtwn4  34385  cvrcmp2  34390  ltcvrntr  34529  atcvrj0  34533  3dim3  34574  paddasslem17  34941  paddass  34943  lautlt  35196  lautcvr  35197  lautj  35198  lautm  35199  erngdvlem3  36097  dvalveclem  36133  mendlmod  37582
  Copyright terms: Public domain W3C validator