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

Theorem 3adant3r1 1196
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 1112 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
323adantr1 1173 1 ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070
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 383  df-3an 1072
This theorem is referenced by:  plttr  17177  pltletr  17178  latjlej1  17272  latjlej2  17273  latnlej  17275  latnlej2  17278  latmlem2  17289  latledi  17296  latjass  17302  latj32  17304  latj13  17305  ipopos  17367  tsrlemax  17427  imasmnd2  17534  grpsubsub  17711  grpnnncan2  17719  imasgrp2  17737  mulgnn0ass  17785  mulgsubdir  17789  cmn32  18417  ablsubadd  18423  imasring  18826  zntoslem  20119  xmettri3  22377  mettri3  22378  xmetrtri  22379  xmetrtri2  22380  metrtri  22381  cphdivcl  23200  cphassr  23230  relogbmulexp  24736  grpodivdiv  27728  grpomuldivass  27729  ablo32  27737  ablodivdiv4  27742  ablodiv32  27743  ablonnncan  27744  nvmdi  27837  dipdi  28032  dipassr  28035  dipsubdir  28037  dipsubdi  28038  dvrcan5  30127  cgr3tr4  32490  cgr3rflx  32492  endofsegid  32523  seglemin  32551  broutsideof2  32560  rngosubdi  34069  rngosubdir  34070  isdrngo2  34082  crngm23  34126  dmncan2  34201  latmassOLD  35031  latm32  35033  cvrnbtwn4  35081  cvrcmp2  35086  ltcvrntr  35225  atcvrj0  35229  3dim3  35270  paddasslem17  35637  paddass  35639  lautlt  35892  lautcvr  35893  lautj  35894  lautm  35895  erngdvlem3  36792  dvalveclem  36828  mendlmod  38282
  Copyright terms: Public domain W3C validator