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

Theorem ad2antrr 479
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
ad2antrr  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ps )

Proof of Theorem ad2antrr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 274 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantlr 468 1  |-  ( ( ( ph  /\  ch )  /\  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:  ad3antrrr  483  simpll  503  simplll  507  simpllr  508  vtoclgft  2710  reupick  3330  euotd  4146  frirrg  4242  ralxfrd  4353  nnsucpred  4500  foun  5354  f1oprg  5379  dffo4  5536  foeqcnvco  5659  fliftfun  5665  isotr  5685  riotass2  5724  ovmpodxf  5864  mpoxopoveq  6105  tfrlem1  6173  tfrlemibacc  6191  tfrlemibfn  6193  tfrlemi14d  6198  tfrexlem  6199  tfr1onlembacc  6207  tfr1onlembfn  6209  tfr1onlemres  6214  tfrcllembacc  6220  tfrcllembfn  6222  tfrcllemres  6227  frecabcl  6264  nnmordi  6380  eroprf  6490  f1imaen2g  6655  xpen  6707  mapen  6708  mapdom1g  6709  mapxpen  6710  xpmapenlem  6711  phplem4dom  6724  nndomo  6726  phpm  6727  fidifsnen  6732  dif1enen  6742  fisbth  6745  fimax2gtrilemstep  6762  fimax2gtri  6763  en2eqpr  6769  unsnfidcex  6776  unsnfidcel  6777  ssfirab  6790  fidcenumlemrks  6809  sbthlemi8  6820  fiuni  6834  ordiso2  6888  updjud  6935  difinfsnlem  6952  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  enumct  6968  enomnilem  6978  fodju0  6987  exmidfodomrlemim  7025  dfplpq2  7130  nqpi  7154  nqnq0pi  7214  nq0nn  7218  elinp  7250  elnp1st2nd  7252  genprndl  7297  genprndu  7298  addnqprllem  7303  addnqprulem  7304  addnqprl  7305  addnqpru  7306  addlocpr  7312  nqprloc  7321  prmuloc  7342  mulnqprl  7344  mulnqpru  7345  mullocpr  7347  distrlem1prl  7358  distrlem1pru  7359  ltsopr  7372  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  aptiprleml  7415  aptiprlemu  7416  archpr  7419  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  archrecpr  7440  caucvgprlemnkj  7442  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprprlemnkltj  7465  caucvgprprlemnkeqj  7466  caucvgprprlemnjltk  7467  caucvgprprlemml  7470  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemdisj  7478  caucvgprprlemexbt  7482  caucvgprprlemexb  7483  caucvgprprlemaddq  7484  suplocexprlemru  7495  suplocexprlemloc  7497  suplocexprlemex  7498  suplocexprlemub  7499  suplocexprlemlub  7500  mulgt0sr  7554  caucvgsrlemcau  7569  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  axsuploc  7805  cnegexlem1  7905  cnegex  7908  apsym  8335  apcotr  8336  apadd1  8337  mulext1  8341  mulge0  8348  apti  8351  aprcl  8375  conjmulap  8456  lemulge11  8588  creui  8682  nndiv  8725  zaddcllemneg  9051  suprzclex  9107  eluzuzle  9290  divfnzn  9369  qapne  9387  xrltso  9537  xrre  9558  xrre3  9560  xaddf  9582  xaddval  9583  xpncan  9609  xleadd1a  9611  xltadd1  9614  xleaddadd  9625  ixxss12  9644  elioc2  9674  elico2  9675  elicc2  9676  fzm1  9835  fzneuz  9836  eluzgtdifelfzo  9929  elfzonelfzo  9962  exfzdc  9972  qtri3or  9975  exbtwnzlemstep  9980  exbtwnzlemex  9982  exbtwnz  9983  modqid  10077  modqcyc2  10088  modqmuladd  10094  modqmuladdnn0  10096  modaddmodlo  10116  addmodlteq  10126  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgsuc  10142  frecuzrdgsuctlem  10151  seq3clss  10195  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemab  10217  iseqf1olemmo  10220  iseqf1olemqf1o  10221  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  seq3f1olemqsumk  10227  seq3f1olemqsum  10228  seq3f1olemp  10230  seq3f1oleml  10231  seq3f1o  10232  seq3id3  10235  ser3ge0  10245  exp3val  10250  expap0  10278  facndiv  10440  faclbnd  10442  bcval5  10464  hashunlem  10505  hashun  10506  hashprg  10509  fiprsshashgt1  10518  hashfacen  10534  zfz1isolemiso  10537  zfz1isolem1  10538  seq3coll  10540  ovshftex  10546  2shfti  10558  seq3shft  10565  cjap  10633  caucvgrelemcau  10707  cvg1nlemcau  10711  cvg1nlemres  10712  recvguniq  10722  resqrexlemdecn  10739  resqrexlemcalc3  10743  resqrexlemcvg  10746  resqrexlemoverl  10748  leabs  10801  absexpzap  10807  ltabs  10814  abslt  10815  absle  10816  maxleim  10932  maxabslemval  10935  fimaxre2  10953  minmax  10956  xrmaxiflemcl  10969  xrmaxifle  10970  xrmaxiflemab  10971  xrmaxiflemlub  10972  xrmaxiflemcom  10973  xrmaxltsup  10982  xrmaxadd  10985  xrminmax  10989  xrbdtri  11000  2clim  11025  climshftlemg  11026  climsqz  11059  climsqz2  11060  climrecvg1n  11072  climcvg1nlem  11073  serf0  11076  sumrbdclem  11100  fsum3cvg  11101  summodclem3  11104  summodclem2a  11105  summodclem2  11106  zsumdc  11108  fsum3  11111  isumss  11115  fisumss  11116  fsum3cvg3  11120  fsumcl2lem  11122  fsumadd  11130  fsumsplit  11131  sumsnf  11133  fsum2d  11159  fisum0diag2  11171  fsummulc2  11172  modfsummod  11182  fsumabs  11189  fsumrelem  11195  fsumiun  11201  geoisumr  11242  cvgratnnlemseq  11250  cvgratz  11256  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcj  11293  efaddlem  11294  tanaddaplem  11359  nndivides  11412  dvdsext  11465  divalglemeunn  11530  divalglemex  11531  divalglemeuneg  11532  zsupcllemstep  11550  infssuzex  11554  dvdsbnd  11557  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlemzz  11602  bezoutlemaz  11603  bezoutlembz  11604  bezoutlemeu  11607  bezoutlemle  11608  bezoutlemsup  11609  dfgcd3  11610  dfgcd2  11614  bezoutr1  11633  dvdslcm  11662  lcmgcdlem  11670  qredeq  11689  qredeu  11690  divgcdcoprm0  11694  divgcdcoprmex  11695  cncongr1  11696  isprm2lem  11709  prmind2  11713  exprmfct  11730  prmdvdsfz  11731  prmexpb  11741  rpexp1i  11744  sqrt2irr  11752  sqne2sq  11766  nonsq  11796  phiprmpw  11809  hashgcdeq  11815  ennnfonelemg  11827  ennnfoneleminc  11835  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemex  11838  ennnfonelemhom  11839  ennnfonelemfun  11841  ennnfonelemf1  11842  ennnfonelemrn  11843  ennnfonelemdm  11844  ennnfonelemnn0  11846  ennnfonelemim  11848  exmidunben  11850  ctinfomlemom  11851  ctinf  11854  ctiunctlemudc  11861  isstruct2r  11881  tgdom  12152  neipsm  12234  tgrest  12249  cnfval  12274  cnpfval  12275  cnpval  12278  iscnp4  12298  cnpnei  12299  cnptopco  12302  cncnpi  12308  cncnp  12310  cnptopresti  12318  cnptoprest2  12320  cndis  12321  lmtopcnp  12330  txbasval  12347  neitx  12348  txcnp  12351  txcnmpt  12353  txcn  12355  imasnopn  12379  psmetres2  12413  isxmet2d  12428  xblss2ps  12484  xblss2  12485  blbas  12513  neibl  12571  metss2lem  12577  metrest  12586  xmettx  12590  metcnp3  12591  metcnp  12592  metcnp2  12593  metcnpi  12595  metcnpi2  12596  mulc1cncf  12656  cncfco  12658  mulcncflem  12670  mulcncf  12671  dedekindeulemuub  12675  dedekindeulemloc  12677  dedekindeulemlu  12679  dedekindeu  12681  suplociccreex  12682  suplociccex  12683  dedekindicclemuub  12684  dedekindicclemloc  12686  dedekindicclemlu  12688  dedekindicclemicc  12690  dedekindicc  12691  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemloc  12699  ivthinc  12701  limcimolemlt  12713  limccnp2lem  12725  limccnp2cntop  12726  limccoap  12727  dvcj  12753  dveflem  12766  sin0pilem1  12773  sin0pilem2  12774  pilem3  12775  coseq0negpitopi  12828  bj-findis  13073  pwle2  13089  pwf1oexmid  13090  nnsf  13095  peano4nninf  13096  nninfalllemn  13098  nninfall  13100  nninfsellemeq  13106  nninfsellemeqinf  13108  qdencn  13118  refeq  13119  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator