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

Theorem ad2antlr 458
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad2antlr  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )

Proof of Theorem ad2antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 261 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 445 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad3antlr  462  simplr  482  simplrl  487  simplrr  488  ordtri2or2exmidlem  4251  en2lp  4278  xpid11m  4557  foun  5145  f1oprg  5168  fcof1o  5429  foeqcnvco  5430  f1eqcocnv  5431  caovord3  5674  f1o2ndf1  5849  smores2  5909  frecrdg  5992  nnaordex  6100  xpdom2  6305  nndomo  6326  phpm  6327  fidifsnen  6331  fientri3  6353  dfplpq2  6452  recclnq  6490  subhalfnqq  6512  distrnq0  6557  prarloclem3step  6594  genpml  6615  genpmu  6616  addnqprl  6627  addnqpru  6628  appdivnq  6661  mulnqprl  6666  mulnqpru  6667  mullocpr  6669  ltexprlemfl  6707  ltexprlemfu  6709  ltmprr  6740  archpr  6741  cauappcvgprlemm  6743  caucvgprlemladdrl  6776  caucvgprprlemopl  6795  caucvgprprlemopu  6797  recexgt0sr  6858  mulgt0sr  6862  elrealeu  6906  axcaucvglemcau  6972  axcaucvglemres  6973  cnegex  7189  apirr  7596  mulge0  7610  lemul12a  7828  lediv2a  7861  creur  7911  nndiv  7954  zaddcllemneg  8284  peano5uzti  8346  divfnzn  8556  xrltso  8717  elioc2  8805  elico2  8806  elicc2  8807  qbtwnzlemstep  9103  qbtwnzlemex  9105  rebtwn2z  9109  caucvgre  9580  resqrexlemlo  9611  cau3lem  9710  qdenre  9798  2clim  9822  cn1lem  9834  climsqz  9855  climsqz2  9856  climcau  9866  sqrt2irr  9878
  Copyright terms: Public domain W3C validator