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

Theorem jctil 310
 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 304 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107 This theorem is referenced by:  jctl  312  ddifnel  3238  unidif  3804  iunxdif2  3897  exss  4186  reg2exmidlema  4491  limom  4571  xpiindim  4720  relssres  4901  funco  5207  nfunsn  5499  fliftcnv  5740  fo1stresm  6103  fo2ndresm  6104  dftpos3  6203  tfri1d  6276  rdgtfr  6315  rdgruledefgg  6316  frectfr  6341  elixpsn  6673  mapxpen  6786  phplem2  6791  sbthlem2  6895  sbthlemi3  6896  djuss  7004  caseinl  7025  caseinr  7026  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  nqprrnd  7446  nqprxx  7449  ltexprlempr  7511  recexprlempr  7535  cauappcvgprlemcl  7556  caucvgprlemcl  7579  caucvgprprlemcl  7607  suplocsrlempr  7710  lemulge11  8720  nn0ge2m1nn  9133  frecfzennn  10307  reccn2ap  11192  demoivreALT  11652  topcld  12469  metrest  12866  pwle2  13531
 Copyright terms: Public domain W3C validator