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

Theorem ad2antrl 459
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1 (φψ)
Assertion
Ref Expression
ad2antrl ((χ (φ θ)) → ψ)

Proof of Theorem ad2antrl
StepHypRef Expression
1 ad2ant.1 . . 3 (φψ)
21adantr 261 . 2 ((φ θ) → ψ)
32adantl 262 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:  simprl  483  simprll  489  simprlr  490  elxp5  4752  f1oprg  5111  cnvf1olem  5787  nnaordi  6017  swoer  6070  0er  6076  enq0sym  6414  nqnq0pi  6420  addlocpr  6518  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  archpr  6614  cauappcvgprlemloc  6623  cauappcvgprlemladdfl  6626  mulcmpblnrlemg  6648  axarch  6753  cnegexlem2  6964  mulge0  7383  divdivap1  7461  divdivap2  7462  conjmulap  7467  ltdivmul  7603  nn0ge0div  8083  peano2uz2  8101  peano5uzti  8102  eluzp1m1  8252  iooshf  8571  divelunit  8620  eluzgtdifelfzo  8803  iseqval  8880  iseqfveq2  8885  expineg2  8898  mulexpzap  8929  leexp2r  8942  expnlbnd2  9007
  Copyright terms: Public domain W3C validator