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

Theorem ad2antrl 479
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 272 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantl 273 1  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simprl  503  simprll  509  simprlr  510  elxp5  4995  f1oprg  5377  cnvf1olem  6087  tfrcl  6227  nnaordi  6370  swoer  6423  0er  6429  mapxpen  6708  fict  6728  dif1enen  6740  php5fin  6742  fin0  6745  fin0or  6746  diffisn  6753  infnfi  6755  unsnfi  6773  fidcenumlemrk  6808  sbthlemi8  6818  fiuni  6832  supmoti  6846  eldju2ndl  6923  eldju2ndr  6924  omp1eomlem  6945  difinfsnlem  6950  ctmlemr  6959  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  enq0sym  7204  nqnq0pi  7210  addlocpr  7308  nqprl  7323  addnqprlemrl  7329  addnqprlemru  7330  mulnqprlemrl  7345  mulnqprlemru  7346  archpr  7415  cauappcvgprlemloc  7424  cauappcvgprlemladdfl  7427  archrecpr  7436  caucvgprlemdisj  7446  caucvgprlemloc  7447  caucvgprprlemml  7466  caucvgprprlemopl  7469  caucvgprprlemdisj  7474  caucvgprprlemloc  7475  suplocexprlemmu  7490  suplocexprlemdisj  7492  mulcmpblnrlemg  7512  caucvgsrlemgt1  7567  axarch  7663  axcaucvglemres  7671  cnegexlem2  7902  mulge0  8344  divdivap1  8446  divdivap2  8447  conjmulap  8452  ltdivmul  8594  nn0ge0div  9092  peano2uz2  9112  peano5uzti  9113  eluzp1m1  9301  xleadd1a  9607  iooshf  9686  divelunit  9736  eluzgtdifelfzo  9925  ioom  9989  modqcyc2  10084  modaddmodup  10111  uzennn  10160  seq3fveq2  10193  seq3id2  10233  seqfeq3  10236  expineg2  10253  mulexpzap  10284  leexp2r  10298  expnlbnd2  10368  hashfacen  10530  resqrexlemp1rp  10729  resqrexlemfp1  10732  negfi  10950  climcaucn  11071  fsum3cvg3  11116  fsum2dlemstep  11154  mptfzshft  11162  expcnvre  11223  moddvds  11409  dvdsflip  11456  addmodlteqALT  11464  nn0o  11511  zsupcllemex  11546  dfgcd2  11609  lcmgcdlem  11665  cncongr1  11691  prmind2  11708  isprm6  11732  cncongrprm  11742  oddpwdclemdc  11757  sqrt2irrap  11764  hashdvds  11803  crth  11806  hashgcdlem  11809  hashgcdeq  11810  ennnfonelemex  11833  setscom  11905  tgcl  12139  lmbr2  12289  txcn  12350  txdis1cn  12353  txlm  12354  hmeoimaf1o  12389  txhmeo  12394  bl2in  12478  blssps  12502  blss  12503  blssexps  12504  blssex  12505  bdxmet  12576  xmetxp  12582  xmetxpbl  12583  xmettx  12585  metcnp3  12586  metcnpi3  12592  dedekindicc  12686  limcimolemlt  12708  qdencn  13056  trilpolemlt1  13068
  Copyright terms: Public domain W3C validator