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  6526  nqprxx  6529  ltexprlempr  6582  recexprlempr  6604  cauappcvgprlemcl  6625  caucvgprlemcl  6647  lemulge11  7613  nn0ge2m1nn  8018  frecfzennn  8884
  Copyright terms: Public domain W3C validator