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

Theorem ad2antrl 474
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad2antrl  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )

Proof of Theorem ad2antrl
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 270 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantl 271 1  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  simprl  498  simprll  504  simprlr  505  elxp5  4919  f1oprg  5295  cnvf1olem  5989  tfrcl  6129  nnaordi  6265  swoer  6318  0er  6324  mapxpen  6562  fict  6582  dif1enen  6594  php5fin  6596  fin0  6599  fin0or  6600  diffisn  6607  infnfi  6609  unsnfi  6627  fidcenumlemrk  6661  sbthlemi8  6671  supmoti  6686  eldju2ndl  6761  eldju2ndr  6762  exmidfodomrlemr  6826  exmidfodomrlemrALT  6827  enq0sym  6989  nqnq0pi  6995  addlocpr  7093  nqprl  7108  addnqprlemrl  7114  addnqprlemru  7115  mulnqprlemrl  7130  mulnqprlemru  7131  archpr  7200  cauappcvgprlemloc  7209  cauappcvgprlemladdfl  7212  archrecpr  7221  caucvgprlemdisj  7231  caucvgprlemloc  7232  caucvgprprlemml  7251  caucvgprprlemopl  7254  caucvgprprlemdisj  7259  caucvgprprlemloc  7260  mulcmpblnrlemg  7284  caucvgsrlemgt1  7338  axarch  7424  axcaucvglemres  7432  cnegexlem2  7656  mulge0  8094  divdivap1  8188  divdivap2  8189  conjmulap  8194  ltdivmul  8335  nn0ge0div  8831  peano2uz2  8851  peano5uzti  8852  eluzp1m1  9040  iooshf  9368  divelunit  9417  eluzgtdifelfzo  9604  ioom  9668  modqcyc2  9763  modaddmodup  9790  iseqval  9867  iseqfveq2  9886  seq3fveq2  9888  seq3id2  9936  iseqid2  9937  expineg2  9960  mulexpzap  9991  leexp2r  10005  expnlbnd2  10075  hashfacen  10237  resqrexlemp1rp  10435  resqrexlemfp1  10438  negfi  10655  climcaucn  10736  fsum3cvg3  10785  fsum2dlemstep  10824  mptfzshft  10832  expcnvre  10893  moddvds  11079  dvdsflip  11126  addmodlteqALT  11134  nn0o  11181  zsupcllemex  11216  dfgcd2  11277  lcmgcdlem  11333  cncongr1  11359  prmind2  11376  isprm6  11400  cncongrprm  11410  oddpwdclemdc  11425  sqrt2irrap  11432  hashdvds  11471  crth  11474  hashgcdlem  11477  hashgcdeq  11478  setscom  11529  qdencn  11870
  Copyright terms: Public domain W3C validator