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

Theorem 3adant3r1 1205
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 1197 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1155 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  plttr  15727  pltletr  15728  latjlej1  15822  latjlej2  15823  latnlej  15825  latnlej2  15828  latmlem2  15839  latledi  15846  latjass  15852  latj32  15854  latj13  15855  ipopos  15917  tsrlemax  15977  imasmnd2  16084  grpsubsub  16254  grpnnncan2  16262  mulgnn0ass  16298  mulgsubdir  16300  imasgrp2  16312  cmn32  16943  ablsubadd  16949  imasring  17395  zntoslem  18722  xmettri3  20982  mettri3  20983  xmetrtri  20984  xmetrtri2  20985  metrtri  20986  cphdivcl  21755  cphassr  21784  grpodivdiv  25377  grpomuldivass  25378  grpopnpcan2  25382  grponnncan2  25383  ablo32  25415  ablodivdiv4  25420  ablodiv32  25421  ablonnncan  25422  nvmdi  25672  nvsubsub23  25684  nvmtri2  25702  dipdi  25885  dipassr  25888  dipsubdir  25890  dipsubdi  25891  dvrcan5  27944  cgr3tr4  29886  cgr3rflx  29888  endofsegid  29919  seglemin  29947  broutsideof2  29956  rngosubdi  30540  rngosubdir  30541  isdrngo2  30545  crngm23  30583  dmncan2  30658  mendlmod  31325  latmassOLD  35076  latm32  35078  cvrnbtwn4  35126  cvrcmp2  35131  ltcvrntr  35270  atcvrj0  35274  3dim3  35315  paddasslem17  35682  paddass  35684  lautlt  35937  lautcvr  35938  lautj  35939  lautm  35940  erngdvlem3  36838  dvalveclem  36874
  Copyright terms: Public domain W3C validator