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  6519  addnqpr1lemrl  6537  addnqpr1lemru  6538  archpr  6613  mulcmpblnrlemg  6628  axarch  6733  cnegexlem2  6944  mulge0  7363  divdivap1  7441  divdivap2  7442  conjmulap  7447  ltdivmul  7583  nn0ge0div  8063  peano2uz2  8081  peano5uzti  8082  eluzp1m1  8232  iooshf  8551  divelunit  8600  eluzgtdifelfzo  8783  iseqval  8860  iseqfveq2  8865  expineg2  8878  mulexpzap  8909  leexp2r  8922  expnlbnd2  8987
  Copyright terms: Public domain W3C validator