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

Theorem jctil 295
Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
Hypotheses
Ref Expression
jctil.1 (φψ)
jctil.2 χ
Assertion
Ref Expression
jctil (φ → (χ ψ))

Proof of Theorem jctil
StepHypRef Expression
1 jctil.2 . . 3 χ
21a1i 9 . 2 (φχ)
3 jctil.1 . 2 (φψ)
42, 3jca 290 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-ia3 101
This theorem is referenced by:  jctl  297  ddifnel  3048  unidif  3582  iunxdif2  3675  exss  3933  onpsssuc  4227  limom  4259  xpiindim  4396  relssres  4571  funco  4862  nfunsn  5128  fliftcnv  5356  fo1stresm  5707  fo2ndresm  5708  dftpos3  5795  tfri1d  5867  rdgruledefgg  5878  frectfr  5896  nqprrnd  6392  nqprlu  6395  ltexprlempr  6439  recexprlempr  6460
  Copyright terms: Public domain W3C validator