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

Theorem 3adant3r1 1233
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 1149 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr1 1210 1 ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 1109
This theorem is referenced by:  plttr  17236  pltletr  17237  latjlej1  17331  latjlej2  17332  latnlej  17334  latnlej2  17337  latmlem2  17348  latledi  17355  latjass  17361  latj32  17363  latj13  17364  ipopos  17426  tsrlemax  17486  imasmnd2  17593  grpsubsub  17771  grpnnncan2  17779  imasgrp2  17797  mulgnn0ass  17842  mulgsubdir  17846  cmn32  18477  ablsubadd  18483  imasring  18886  zntoslem  20177  xmettri3  22437  mettri3  22438  xmetrtri  22439  xmetrtri2  22440  metrtri  22441  cphdivcl  23260  cphassr  23290  relogbmulexp  24807  grpodivdiv  27851  grpomuldivass  27852  ablo32  27860  ablodivdiv4  27865  ablodiv32  27866  nvmdi  27959  dipdi  28154  dipassr  28157  dipsubdir  28159  dipsubdi  28160  dvrcan5  30240  cgr3tr4  32603  cgr3rflx  32605  endofsegid  32636  seglemin  32664  broutsideof2  32673  rngosubdi  34166  rngosubdir  34167  isdrngo2  34179  crngm23  34223  dmncan2  34298  latmassOLD  35185  latm32  35187  cvrnbtwn4  35235  cvrcmp2  35240  ltcvrntr  35380  atcvrj0  35384  3dim3  35425  paddasslem17  35792  paddass  35794  lautlt  36047  lautcvr  36048  lautj  36049  lautm  36050  erngdvlem3  36946  dvalveclem  36981  mendlmod  38440
  Copyright terms: Public domain W3C validator