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

Theorem ad2antrl 490
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 276 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantl 277 1  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  simprl  529  simprll  537  simprlr  538  elxp5  5112  f1oprg  5500  cnvf1olem  6218  tfrcl  6358  nnaordi  6502  swoer  6556  0er  6562  mapxpen  6841  fict  6861  dif1enen  6873  php5fin  6875  fin0  6878  fin0or  6879  diffisn  6886  infnfi  6888  unsnfi  6911  fidcenumlemrk  6946  sbthlemi8  6956  fiuni  6970  supmoti  6985  eldju2ndl  7064  eldju2ndr  7065  omp1eomlem  7086  difinfsnlem  7091  ctmlemr  7100  nninfwlpor  7165  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  enq0sym  7409  nqnq0pi  7415  addlocpr  7513  nqprl  7528  addnqprlemrl  7534  addnqprlemru  7535  mulnqprlemrl  7550  mulnqprlemru  7551  archpr  7620  cauappcvgprlemloc  7629  cauappcvgprlemladdfl  7632  archrecpr  7641  caucvgprlemdisj  7651  caucvgprlemloc  7652  caucvgprprlemml  7671  caucvgprprlemopl  7674  caucvgprprlemdisj  7679  caucvgprprlemloc  7680  suplocexprlemmu  7695  suplocexprlemdisj  7697  mulcmpblnrlemg  7717  caucvgsrlemgt1  7772  axarch  7868  axcaucvglemres  7876  cnegexlem2  8110  mulge0  8553  divdivap1  8656  divdivap2  8657  conjmulap  8662  ltdivmul  8809  nn0ge0div  9316  peano2uz2  9336  peano5uzti  9337  eluzp1m1  9527  xleadd1a  9847  iooshf  9926  divelunit  9976  eluzgtdifelfzo  10170  ioom  10234  modqcyc2  10333  modaddmodup  10360  uzennn  10409  seq3fveq2  10442  seq3id2  10482  seqfeq3  10485  expineg2  10502  mulexpzap  10533  leexp2r  10547  expnlbnd2  10618  hashfacen  10787  resqrexlemp1rp  10986  resqrexlemfp1  10989  negfi  11207  climcaucn  11330  fsum3cvg3  11375  fsum2dlemstep  11413  mptfzshft  11421  expcnvre  11482  fprodrev  11598  fprod2dlemstep  11601  moddvds  11777  dvdsflip  11827  addmodlteqALT  11835  nn0o  11882  zsupcllemex  11917  dfgcd2  11985  lcmgcdlem  12047  cncongr1  12073  prmind2  12090  isprm5lem  12111  isprm6  12117  cncongrprm  12127  oddpwdclemdc  12143  sqrt2irrap  12150  hashdvds  12191  crth  12194  prmdiveq  12206  hashgcdlem  12208  hashgcdeq  12209  pclem0  12256  pclemub  12257  pcprendvds2  12261  pcmul  12271  pcexp  12279  pcneg  12294  pc2dvds  12299  pcmpt  12311  prmpwdvds  12323  pockthg  12325  1arith  12335  4sqlem2  12357  ennnfonelemex  12385  setscom  12472  insubm  12749  isgrpinv  12803  tgcl  13197  lmbr2  13347  txcn  13408  txdis1cn  13411  txlm  13412  hmeoimaf1o  13447  txhmeo  13452  bl2in  13536  blssps  13560  blss  13561  blssexps  13562  blssex  13563  bdxmet  13634  xmetxp  13640  xmetxpbl  13641  xmettx  13643  metcnp3  13644  metcnpi3  13650  dedekindicc  13744  limcimolemlt  13766  rprelogbmul  14006  logbgcd1irr  14018  lgsne0  14072  2sqlem8  14092  qdencn  14398  trilpolemlt1  14412
  Copyright terms: Public domain W3C validator