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  3069  unidif  3603  iunxdif2  3696  exss  3954  onpsssuc  4247  limom  4279  xpiindim  4416  relssres  4591  funco  4883  nfunsn  5150  fliftcnv  5378  fo1stresm  5730  fo2ndresm  5731  dftpos3  5818  tfri1d  5890  rdgtfr  5901  rdgruledefgg  5902  frectfr  5924  nqprrnd  6525  nqprxx  6528  ltexprlempr  6581  recexprlempr  6603  cauappcvgprlemcl  6624  lemulge11  7593  nn0ge2m1nn  7998  frecfzennn  8864
  Copyright terms: Public domain W3C validator