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

Theorem ad2antrl 467
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 265 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantl 266 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:  simprl  491  simprll  497  simprlr  498  elxp5  4837  f1oprg  5196  cnvf1olem  5873  nnaordi  6112  swoer  6165  0er  6171  php5fin  6370  fin0  6373  fin0or  6374  diffisn  6381  supmoti  6399  enq0sym  6588  nqnq0pi  6594  addlocpr  6692  nqprl  6707  addnqprlemrl  6713  addnqprlemru  6714  mulnqprlemrl  6729  mulnqprlemru  6730  archpr  6799  cauappcvgprlemloc  6808  cauappcvgprlemladdfl  6811  archrecpr  6820  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprprlemml  6850  caucvgprprlemopl  6853  caucvgprprlemdisj  6858  caucvgprprlemloc  6859  mulcmpblnrlemg  6883  caucvgsrlemgt1  6937  axarch  7023  axcaucvglemres  7031  cnegexlem2  7250  mulge0  7684  divdivap1  7774  divdivap2  7775  conjmulap  7780  ltdivmul  7917  nn0ge0div  8385  peano2uz2  8404  peano5uzti  8405  eluzp1m1  8592  iooshf  8922  divelunit  8971  eluzgtdifelfzo  9155  ioom  9217  modqcyc2  9310  modaddmodup  9337  iseqval  9384  iseqfveq2  9392  expineg2  9429  mulexpzap  9460  leexp2r  9474  expnlbnd2  9542  resqrexlemp1rp  9833  resqrexlemfp1  9836  climcaucn  10101  moddvds  10117  dvdsflip  10163  addmodlteqALT  10171  nn0o  10219  oddpwdclemdc  10261  qdencn  10511
  Copyright terms: Public domain W3C validator