ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jctil 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  3075  unidif  3612  iunxdif2  3705  exss  3963  reg2exmidlema  4259  onpsssuc  4295  limom  4336  xpiindim  4473  relssres  4648  funco  4940  nfunsn  5207  fliftcnv  5435  fo1stresm  5788  fo2ndresm  5789  dftpos3  5877  tfri1d  5949  rdgtfr  5961  rdgruledefgg  5962  frectfr  5985  phplem2  6316  nqprrnd  6641  nqprxx  6644  ltexprlempr  6706  recexprlempr  6730  cauappcvgprlemcl  6751  caucvgprlemcl  6774  caucvgprprlemcl  6802  lemulge11  7832  nn0ge2m1nn  8242  frecfzennn  9203
  Copyright terms: Public domain W3C validator