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

Theorem 3ad2antr1 1120
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antr1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )

Proof of Theorem 3ad2antr1
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantrr 697 . 2  |-  ( (
ph  /\  ( ch  /\ 
ps ) )  ->  th )
323adantr3 1116 1  |-  ( (
ph  /\  ( ch  /\ 
ps  /\  ta )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ispod  4322  dfwe2  4573  poxp  6227  cfcoflem  7898  axdc3lem  8076  fzosubel2  10909  sqr0lem  11726  iscatd2  13583  curf2cl  14005  yonedalem4c  14051  grpsubadd  14553  mulgnnass  14595  mulgnn0ass  14596  dprdss  15264  dprd2da  15277  lsssn0  15705  psrbaglesupp  16114  zntoslem  16510  blsscls  18053  iimulcl  18435  pi1grplem  18547  pi1xfrf  18551  dvconst  19266  logexprlim  20464  nvss  21149  disjdsct  23369  issgon  23484  measdivcstOLD  23551  measdivcst  23552  grpodlcan  25376  ismonb2  25812  isepib2  25822  fzadd2  26444  fdc  26455  cvrnbtwn3  29466  paddasslem9  30017  paddasslem17  30025  pmapjlln1  30044  lautj  30282  lautm  30283
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