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

Theorem 3adant1r 1212
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant1r  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3adant1r
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1189 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 714 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1184 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  3adant2r  1214  3adant3r  1216  ecopovtrn  7316  isf32lem9  8644  axdc3lem4  8736  tskun  9067  dvdscmulr  13682  divalglem8  13725  divscrng  17448  dvfsumlem3  21636  dvfsumrlim  21639  dvfsumrlim2  21640  dvfsumrlim3  21641  dchrisumlem3  22876  dchrisum  22877  abvcxp  23000  padicabv  23015  hvmulcan  24646  isarchi2  26367  archiabllem2c  26377  hasheuni  26699  pellex  29344  refsumcn  29920  fmuldfeq  29932  stoweidlem31  29994  stoweidlem43  30006  stoweidlem46  30009  stoweidlem52  30015  stoweidlem53  30016  stoweidlem54  30017  stoweidlem55  30018  stoweidlem56  30019  stoweidlem57  30020  stoweidlem58  30021  stoweidlem59  30022  stoweidlem60  30023  stoweidlem62  30025  stoweid  30026  el0ldep  31152  tendoicl  34798  cdlemkfid2N  34925  erngdvlem4  34993
  Copyright terms: Public domain W3C validator