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

Theorem 3adant1r 1221
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 1197 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 714 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1192 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:  3adant2r  1223  3adant3r  1225  ecopovtrn  7426  isf32lem9  8753  axdc3lem4  8845  tskun  9176  dvdscmulr  13890  divalglem8  13934  ghmgrp  16066  quscrng  17758  dvfsumlem3  22297  dvfsumrlim  22300  dvfsumrlim2  22301  dvfsumrlim3  22302  dchrisumlem3  23542  dchrisum  23543  abvcxp  23666  padicabv  23681  hvmulcan  25812  isarchi2  27553  archiabllem2c  27563  hasheuni  27916  pellex  30699  refsumcn  31307  ssfiunibd  31409  fmuldfeq  31456  cosknegpi  31528  stoweidlem31  31654  stoweidlem43  31666  stoweidlem46  31669  stoweidlem52  31675  stoweidlem53  31676  stoweidlem54  31677  stoweidlem55  31678  stoweidlem56  31679  stoweidlem57  31680  stoweidlem58  31681  stoweidlem59  31682  stoweidlem60  31683  stoweidlem62  31685  stoweid  31686  fourierdlem12  31742  fourierdlem41  31771  fourierdlem48  31778  fourierdlem79  31809  fourierdlem81  31811  el0ldep  32549  tendoicl  35993  cdlemkfid2N  36120  erngdvlem4  36188
  Copyright terms: Public domain W3C validator