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

Theorem ad2antlr 466
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
ad2antlr (((𝜒𝜑) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 265 . 2 ((𝜑𝜃) → 𝜓)
32adantll 453 1 (((𝜒𝜑) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad3antlr  470  simplr  490  simplrl  495  simplrr  496  ordtri2or2exmidlem  4278  en2lp  4305  xpid11m  4584  foun  5172  f1oprg  5195  fcof1o  5456  foeqcnvco  5457  f1eqcocnv  5458  caovord3  5701  f1o2ndf1  5876  smores2  5939  frecrdg  6022  nnaordex  6130  xpdom2  6335  nndomo  6356  phpm  6357  fidifsnen  6361  fientri3  6383  dfplpq2  6509  recclnq  6547  subhalfnqq  6569  distrnq0  6614  prarloclem3step  6651  genpml  6672  genpmu  6673  addnqprl  6684  addnqpru  6685  appdivnq  6718  mulnqprl  6723  mulnqpru  6724  mullocpr  6726  ltexprlemfl  6764  ltexprlemfu  6766  ltmprr  6797  archpr  6798  cauappcvgprlemm  6800  caucvgprlemladdrl  6833  caucvgprprlemopl  6852  caucvgprprlemopu  6854  recexgt0sr  6915  mulgt0sr  6919  elrealeu  6963  axcaucvglemcau  7029  axcaucvglemres  7030  cnegex  7251  apirr  7669  mulge0  7683  lemul12a  7902  lediv2a  7935  creur  7986  nndiv  8029  zaddcllemneg  8340  peano5uzti  8404  divfnzn  8652  xrltso  8817  elioc2  8905  elico2  8906  elicc2  8907  qbtwnzlemstep  9204  qbtwnzlemex  9206  rebtwn2z  9210  modqid  9293  modqcyc  9303  mulqaddmodid  9308  modqadd2mod  9318  addmodlteq  9342  facndiv  9600  faclbnd  9602  ibcval5  9624  caucvgre  9801  resqrexlemlo  9832  cau3lem  9933  qdenre  10021  2clim  10045  cn1lem  10057  climsqz  10078  climsqz2  10079  climcau  10089  dvdseq  10152  dvdsext  10159  odd2np1  10176  sqoddm1div8z  10190  nno  10210  sqrt2irr  10223
  Copyright terms: Public domain W3C validator