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

Theorem ad2antrr 472
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 (𝜑𝜓)
Assertion
Ref Expression
ad2antrr (((𝜑𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 270 . 2 ((𝜑𝜃) → 𝜓)
32adantlr 461 1 (((𝜑𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  ad3antrrr  476  simpll  496  simplll  500  simpllr  501  vtoclgft  2663  reupick  3272  euotd  4055  frirrg  4151  ralxfrd  4258  foun  5235  f1oprg  5258  dffo4  5410  foeqcnvco  5530  fliftfun  5536  isotr  5556  riotass2  5595  ovmpt2dxf  5727  mpt2xopoveq  5959  tfrlem1  6027  tfrlemibacc  6045  tfrlemibfn  6047  tfrlemi14d  6052  tfrexlem  6053  tfr1onlembacc  6061  tfr1onlembfn  6063  tfr1onlemres  6068  tfrcllembacc  6074  tfrcllembfn  6076  tfrcllemres  6081  frecabcl  6118  nnmordi  6227  eroprf  6337  f1imaen2g  6462  xpen  6513  mapen  6514  mapdom1g  6515  mapxpen  6516  xpmapenlem  6517  phplem4dom  6530  nndomo  6532  phpm  6533  fidifsnen  6538  dif1enen  6548  fisbth  6551  fimax2gtrilemstep  6568  fimax2gtri  6569  en2eqpr  6575  unsnfidcex  6582  unsnfidcel  6583  ssfirab  6593  sbthlemi8  6617  ordiso2  6672  updjud  6717  enomnilem  6738  fodjuomnilem0  6746  exmidfodomrlemim  6771  dfplpq2  6857  nqpi  6881  nqnq0pi  6941  nq0nn  6945  elinp  6977  elnp1st2nd  6979  genprndl  7024  genprndu  7025  addnqprllem  7030  addnqprulem  7031  addnqprl  7032  addnqpru  7033  addlocpr  7039  nqprloc  7048  prmuloc  7069  mulnqprl  7071  mulnqpru  7072  mullocpr  7074  distrlem1prl  7085  distrlem1pru  7086  ltsopr  7099  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemloc  7110  ltexprlemrl  7113  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  archpr  7146  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  archrecpr  7167  caucvgprlemnkj  7169  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnjltk  7194  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemdisj  7205  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  mulgt0sr  7267  caucvgsrlemcau  7282  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  axcaucvglemcau  7377  axcaucvglemres  7378  cnegexlem1  7601  cnegex  7604  apsym  8024  apcotr  8025  apadd1  8026  mulext1  8030  mulge0  8037  apti  8040  conjmulap  8135  lemulge11  8262  creui  8355  nndiv  8397  zaddcllemneg  8722  suprzclex  8777  eluzuzle  8959  divfnzn  9038  qapne  9056  xrltso  9198  xrre  9214  xrre3  9216  ixxss12  9256  elioc2  9286  elico2  9287  elicc2  9288  fzm1  9444  fzneuz  9445  eluzgtdifelfzo  9536  elfzonelfzo  9569  exfzdc  9579  qtri3or  9582  exbtwnzlemstep  9587  exbtwnzlemex  9589  exbtwnz  9590  modqid  9684  modqcyc2  9695  modqmuladd  9701  modqmuladdnn0  9703  modaddmodlo  9723  addmodlteq  9733  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgsuc  9749  frecuzrdgsuctlem  9758  iseqoveq  9798  iseqf1olemqcl  9819  iseqf1olemnab  9821  iseqf1olemab  9822  iseqf1olemmo  9825  iseqf1olemqf1o  9826  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemqsumk  9832  iseqf1olemqsum  9833  iseqf1olemp  9835  iseqf1oleml  9836  iseqf1o  9837  iseqid3s  9841  expival  9855  expap0  9883  facndiv  10043  faclbnd  10045  ibcval5  10067  hashunlem  10108  hashun  10109  hashprg  10112  fiprsshashgt1  10121  hashfacen  10137  zfz1isolemiso  10140  zfz1isolem1  10141  iseqcoll  10143  ovshftex  10149  2shfti  10161  cjap  10235  caucvgrelemcau  10308  cvg1nlemcau  10312  cvg1nlemres  10313  recvguniq  10323  resqrexlemdecn  10340  resqrexlemcalc3  10344  resqrexlemcvg  10347  resqrexlemoverl  10349  leabs  10402  absexpzap  10408  ltabs  10415  abslt  10416  absle  10417  maxleim  10533  maxabslemval  10536  fimaxre2  10551  minmax  10554  2clim  10582  climshftlemg  10583  climsqz  10615  climsqz2  10616  climrecvg1n  10627  climcvg1nlem  10628  serif0  10631  isumrblem  10655  fisumcvg  10656  isummolem3  10659  isummolem2a  10660  isummolem2  10661  zisum  10663  fisum  10665  isumss  10669  fisumss  10670  nndivides  10678  dvdsext  10731  divalglemeunn  10796  divalglemex  10797  divalglemeuneg  10798  zsupcllemstep  10816  infssuzex  10820  dvdsbnd  10823  bezoutlemnewy  10860  bezoutlemstep  10861  bezoutlemmain  10862  bezoutlemzz  10866  bezoutlemaz  10867  bezoutlembz  10868  bezoutlemeu  10871  bezoutlemle  10872  bezoutlemsup  10873  dfgcd3  10874  dfgcd2  10878  bezoutr1  10897  dvdslcm  10926  lcmgcdlem  10934  qredeq  10953  qredeu  10954  divgcdcoprm0  10958  divgcdcoprmex  10959  cncongr1  10960  isprm2lem  10973  prmind2  10977  exprmfct  10994  prmdvdsfz  10995  prmexpb  11005  rpexp1i  11008  sqrt2irr  11016  sqne2sq  11030  nonsq  11060  phiprmpw  11073  hashgcdeq  11079  bj-findis  11312  nnsucpred  11329  nnsf  11333  peano4nninf  11334  nninfalllemn  11336  nninfall  11338  nninfsellemeq  11344  nninfsellemeqinf  11346  qdencn  11353
  Copyright terms: Public domain W3C validator