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

Theorem ad2antlr 466
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 265 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 453 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  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:  ad3antlr  470  simplr  490  simplrl  495  simplrr  496  ordtri2or2exmidlem  4279  en2lp  4306  xpid11m  4585  foun  5173  f1oprg  5196  fcof1o  5457  foeqcnvco  5458  f1eqcocnv  5459  caovord3  5702  f1o2ndf1  5877  smores2  5940  frecrdg  6023  nnaordex  6131  xpdom2  6336  nndomo  6357  phpm  6358  fidifsnen  6362  fientri3  6384  dfplpq2  6510  recclnq  6548  subhalfnqq  6570  distrnq0  6615  prarloclem3step  6652  genpml  6673  genpmu  6674  addnqprl  6685  addnqpru  6686  appdivnq  6719  mulnqprl  6724  mulnqpru  6725  mullocpr  6727  ltexprlemfl  6765  ltexprlemfu  6767  ltmprr  6798  archpr  6799  cauappcvgprlemm  6801  caucvgprlemladdrl  6834  caucvgprprlemopl  6853  caucvgprprlemopu  6855  recexgt0sr  6916  mulgt0sr  6920  elrealeu  6964  axcaucvglemcau  7030  axcaucvglemres  7031  cnegex  7252  apirr  7670  mulge0  7684  lemul12a  7903  lediv2a  7936  creur  7987  nndiv  8030  zaddcllemneg  8341  peano5uzti  8405  divfnzn  8653  xrltso  8818  elioc2  8906  elico2  8907  elicc2  8908  qbtwnzlemstep  9205  qbtwnzlemex  9207  rebtwn2z  9211  modqid  9299  modqcyc  9309  mulqaddmodid  9314  modqadd2mod  9324  addmodlteq  9348  facndiv  9607  faclbnd  9609  ibcval5  9631  caucvgre  9808  resqrexlemlo  9840  cau3lem  9941  qdenre  10029  2clim  10053  cn1lem  10065  climsqz  10086  climsqz2  10087  climcau  10097  dvdseq  10160  dvdsext  10167  odd2np1  10184  sqoddm1div8z  10198  nno  10218  sqrt2irr  10251
  Copyright terms: Public domain W3C validator