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

Theorem ad2antrr 457
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 261 . 2 ((φ θ) → ψ)
32adantlr 446 1 (((φ χ) θ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad3antrrr  461  simpll  481  simplll  485  simpllr  486  vtoclgft  2598  reupick  3215  euotd  3982  ralxfrd  4160  foun  5088  f1oprg  5111  dffo4  5258  foeqcnvco  5373  fliftfun  5379  isotr  5399  riotass2  5437  ovmpt2dxf  5568  mpt2xopoveq  5796  tfrlem1  5864  tfrlemibacc  5881  tfrlemibfn  5883  tfrlemi14d  5888  tfrexlem  5889  nnmordi  6025  eroprf  6135  f1imaen2g  6209  dfplpq2  6338  nqpi  6362  nqnq0pi  6421  nq0nn  6425  elinp  6457  elnp1st2nd  6459  genprndl  6504  genprndu  6505  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  addlocpr  6519  nqprloc  6528  prmuloc  6547  mulnqprl  6549  mulnqpru  6550  mullocpr  6552  distrlem1prl  6558  distrlem1pru  6559  ltsopr  6570  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  aptiprleml  6611  aptiprlemu  6612  archpr  6615  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  caucvgprlemnkj  6637  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemladdfu  6648  mulgt0sr  6704  cnegexlem1  6983  cnegex  6986  apsym  7390  apcotr  7391  apadd1  7392  mulext1  7396  mulge0  7403  apti  7406  conjmulap  7487  lemulge11  7613  creui  7693  nndiv  7735  zaddcllemneg  8060  eluzuzle  8257  divfnzn  8332  qapne  8350  xrltso  8487  xrre  8503  xrre3  8505  ixxss12  8545  elioc2  8575  elico2  8576  elicc2  8577  fzm1  8732  fzneuz  8733  eluzgtdifelfzo  8823  elfzonelfzo  8856  frecuzrdgrrn  8875  expival  8911  expap0  8939  cjap  9134  bj-findis  9439
  Copyright terms: Public domain W3C validator