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

Theorem ad2antlr 478
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 272 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 465 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:  ad3antlr  482  simplr  502  simplrl  507  simplrr  508  ordtri2or2exmidlem  4409  en2lp  4437  foun  5352  f1oprg  5377  fcof1o  5656  foeqcnvco  5657  f1eqcocnv  5658  caovord3  5910  f1o2ndf1  6091  smores2  6157  frecrdg  6271  nnaordex  6389  xpdom2  6691  xpen  6705  mapen  6706  xpmapenlem  6709  nndomo  6724  phpm  6725  fidifsnen  6730  isinfinf  6757  finexdc  6762  fientri3  6769  fiintim  6783  xpfi  6784  f1dmvrnfibi  6798  sbthlemi8  6818  djudom  6944  omp1eomlem  6945  difinfsn  6951  ctmlemr  6959  ctssdccl  6962  enomnilem  6976  finomni  6978  ismkvnex  6995  exmidfodomrlemrALT  7023  dfplpq2  7126  recclnq  7164  subhalfnqq  7186  distrnq0  7231  prarloclem3step  7268  genpml  7289  genpmu  7290  addnqprl  7301  addnqpru  7302  appdivnq  7335  mulnqprl  7340  mulnqpru  7341  mullocpr  7343  ltexprlemfl  7381  ltexprlemfu  7383  ltmprr  7414  archpr  7415  cauappcvgprlemm  7417  caucvgprlemladdrl  7450  caucvgprprlemopl  7469  caucvgprprlemopu  7471  recexgt0sr  7545  mulgt0sr  7550  elrealeu  7601  axcaucvglemcau  7670  axcaucvglemres  7671  cnegex  7904  apirr  8330  mulge0  8344  lemul12a  8577  lediv2a  8610  creur  8674  nndiv  8718  zaddcllemneg  9044  peano5uzti  9110  supinfneg  9339  infsupneg  9340  divfnzn  9362  xrltso  9522  xpncan  9594  xltadd1  9599  xleaddadd  9610  elioc2  9659  elico2  9660  elicc2  9661  exfzdc  9957  exbtwnzlemex  9967  rebtwn2z  9972  modqid  10062  modqcyc  10072  mulqaddmodid  10077  modqadd2mod  10087  addmodlteq  10111  frecuzrdgg  10129  seq3val  10171  seqvalcd  10172  seq3clss  10180  iseqf1olemqcl  10199  iseqf1olemnab  10201  seq3f1olemp  10215  seq3f1o  10217  fser0const  10229  ser3ge0  10230  exp3vallem  10234  facndiv  10425  faclbnd  10427  bcval5  10449  hashen  10470  fihashdom  10489  hashunlem  10490  hashfacen  10519  zfz1isolemiso  10522  seq3coll  10525  caucvgre  10693  resqrexlemlo  10725  cau3lem  10826  qdenre  10914  rexico  10933  fimaxre2  10938  xrmaxiflemcl  10954  xrmaxifle  10955  xrmaxiflemcom  10958  2clim  11010  cn1lem  11023  climsqz  11044  climsqz2  11045  climcau  11056  sumrbdclem  11085  summodclem2a  11090  fsum3  11096  fsumcl2lem  11107  fsumadd  11115  sumsnf  11118  fsum2dlemstep  11143  fisum0diag2  11156  fsummulc2  11157  mertenslemub  11243  mertenslemi1  11244  mertensabs  11246  efaddlem  11279  tanaddaplem  11344  zdvdsdc  11410  dvdseq  11442  dvdsext  11449  odd2np1  11466  sqoddm1div8z  11479  nno  11499  zsupcllemstep  11534  infssuzex  11538  dfgcd3  11594  dvdslcm  11646  lcmneg  11651  lcmgcdlem  11654  ncoprmgcdne1b  11666  qredeq  11673  qredeu  11674  divgcdcoprm0  11678  exprmfct  11714  prmdvdsfz  11715  rpexp1i  11728  sqrt2irr  11736  nonsq  11780  ctinfom  11836  enctlem  11840  setsfun  11889  setsfun0  11890  setscom  11894  tgdom  12136  ssrest  12246  cnfval  12258  cnpfval  12259  cnpval  12262  iscnp3  12267  ssidcn  12274  cnpnei  12283  cnntr  12289  cncnp  12294  cnptopresti  12302  tx1cn  12333  upxp  12336  imasnopn  12363  bdmet  12566  metcnp  12576  dvrecap  12720  nnsf  13001  peano4nninf  13002  nninfalllemn  13004  nninfalllem1  13005  nninfsellemqall  13013  nninfsellemeqinf  13014  nninffeq  13018  exmidsbthrlem  13019
  Copyright terms: Public domain W3C validator