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

Theorem jctil 312
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 306 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  jctl  314  ddifnel  3278  unidif  3853  iunxdif2  3947  exss  4239  reg2exmidlema  4545  limom  4625  xpiindim  4776  relssres  4957  funco  5268  nfunsn  5561  fliftcnv  5809  fo1stresm  6175  fo2ndresm  6176  dftpos3  6276  tfri1d  6349  rdgtfr  6388  rdgruledefgg  6389  frectfr  6414  elixpsn  6748  mapxpen  6861  phplem2  6866  sbthlem2  6970  sbthlemi3  6971  djuss  7082  caseinl  7103  caseinr  7104  exmidfodomrlemr  7214  exmidfodomrlemrALT  7215  2omotaplemap  7269  nqprrnd  7555  nqprxx  7558  ltexprlempr  7620  recexprlempr  7644  cauappcvgprlemcl  7665  caucvgprlemcl  7688  caucvgprprlemcl  7716  suplocsrlempr  7819  lemulge11  8836  nn0ge2m1nn  9249  frecfzennn  10439  reccn2ap  11334  demoivreALT  11794  pcdiv  12315  subrgid  13438  topcld  13880  metrest  14277  pwle2  15020
  Copyright terms: Public domain W3C validator