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

Theorem 3adant3r1 1160
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant3r1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )

Proof of Theorem 3adant3r1
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1152 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1114 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  plttr  14104  pltletr  14105  joinle  14127  latjlej1  14171  latjlej2  14172  latnlej  14174  latnlej2  14177  latmlem2  14188  latledi  14195  latjass  14201  latj32  14203  latj13  14204  ipopos  14263  tsrlemax  14329  imasmnd2  14409  grpsubsub  14554  grpnnncan2  14561  mulgnn0ass  14596  mulgsubdir  14598  imasgrp2  14610  cmn32  15107  ablsubadd  15113  imasrng  15402  zntoslem  16510  xmettri3  17917  mettri3  17918  xmetrtri  17919  xmetrtri2  17920  metrtri  17921  cphdivcl  18618  cphassr  18647  grpodivdiv  20915  grpomuldivass  20916  grpopnpcan2  20920  grponnncan2  20921  ablo32  20953  ablodivdiv4  20958  ablodiv32  20959  ablonnncan  20960  nvmdi  21208  nvsubsub23  21220  nvmtri2  21238  dipdi  21421  dipassr  21424  dipsubdir  21426  dipsubdi  21427  cgr3tr4  24675  cgr3rflx  24677  endofsegid  24708  seglemin  24736  broutsideof2  24745  grpodrcan  25375  dblsubvec  25474  mvecrtol2  25477  addassv  25656  cmpassoh  25801  homgrf  25802  rngosubdi  26584  rngosubdir  26585  isdrngo2  26589  crngm23  26627  dmncan2  26702  mendlmod  27501  latmassOLD  29419  latm32  29421  cvrnbtwn4  29469  cvrcmp2  29474  ltcvrntr  29613  atcvrj0  29617  3dim3  29658  paddasslem17  30025  paddass  30027  lautlt  30280  lautcvr  30281  lautj  30282  lautm  30283  erngdvlem3  31179  dvalveclem  31215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator