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

Theorem 3adant3r1 1214
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 1206 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr1 1164 1  |-  ( (
ph  /\  ( ta  /\ 
ps  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  plttr  16167  pltletr  16168  latjlej1  16262  latjlej2  16263  latnlej  16265  latnlej2  16268  latmlem2  16279  latledi  16286  latjass  16292  latj32  16294  latj13  16295  ipopos  16357  tsrlemax  16417  imasmnd2  16524  grpsubsub  16694  grpnnncan2  16702  mulgnn0ass  16738  mulgsubdir  16740  imasgrp2  16752  cmn32  17383  ablsubadd  17389  imasring  17782  zntoslem  19058  xmettri3  21299  mettri3  21300  xmetrtri  21301  xmetrtri2  21302  metrtri  21303  cphdivcl  22053  cphassr  22082  relogbmulexp  23580  grpodivdiv  25821  grpomuldivass  25822  grpopnpcan2  25826  grponnncan2  25827  ablo32  25859  ablodivdiv4  25864  ablodiv32  25865  ablonnncan  25866  nvmdi  26116  nvsubsub23  26128  nvmtri2  26146  dipdi  26329  dipassr  26332  dipsubdir  26334  dipsubdi  26335  dvrcan5  28395  cgr3tr4  30604  cgr3rflx  30606  endofsegid  30637  seglemin  30665  broutsideof2  30674  rngosubdi  31895  rngosubdir  31896  isdrngo2  31900  crngm23  31938  dmncan2  32013  latmassOLD  32503  latm32  32505  cvrnbtwn4  32553  cvrcmp2  32558  ltcvrntr  32697  atcvrj0  32701  3dim3  32742  paddasslem17  33109  paddass  33111  lautlt  33364  lautcvr  33365  lautj  33366  lautm  33367  erngdvlem3  34265  dvalveclem  34301  mendlmod  35757
  Copyright terms: Public domain W3C validator