ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad3antrrr Unicode version

Theorem ad3antrrr 469
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad3antrrr  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem ad3antrrr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 265 . 2  |-  ( (
ph  /\  ch )  ->  ps )
32ad2antrr 465 1  |-  ( ( ( ( ph  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad4antr  471  phplem4on  6360  ltaddpr  6753  ltexprlemrl  6766  addcanprleml  6770  addcanprlemu  6771  aptiprleml  6795  aptiprlemu  6796  cauappcvgprlemdisj  6807  cauappcvgprlemladdrl  6813  caucvgprlemloc  6831  caucvgprlemladdrl  6834  caucvgprprlemopl  6853  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  caucvgsrlemoffres  6942  axcaucvglemcau  7030  axcaucvglemres  7031  apreim  7668  apsym  7671  apcotr  7672  apadd1  7673  apneg  7676  mulext1  7677  mulge0  7684  apti  7687  qapne  8671  qtri3or  9200  qbtwnzlemstep  9205  rebtwn2zlemstep  9209  addmodlteq  9348  faclbnd  9609  cvg1nlemres  9812  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemga  9850  climrecvg1n  10098  serif0  10102  dvds2ln  10140  divalglemeunn  10233  divalglemeuneg  10235
  Copyright terms: Public domain W3C validator