Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  jctil GIF 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  3208  unidif  3772  iunxdif2  3865  exss  4153  reg2exmidlema  4453  limom  4531  xpiindim  4680  relssres  4861  funco  5167  nfunsn  5459  fliftcnv  5700  fo1stresm  6063  fo2ndresm  6064  dftpos3  6163  tfri1d  6236  rdgtfr  6275  rdgruledefgg  6276  frectfr  6301  elixpsn  6633  mapxpen  6746  phplem2  6751  sbthlem2  6850  sbthlemi3  6851  djuss  6959  caseinl  6980  caseinr  6981  exmidfodomrlemr  7071  exmidfodomrlemrALT  7072  nqprrnd  7371  nqprxx  7374  ltexprlempr  7436  recexprlempr  7460  cauappcvgprlemcl  7481  caucvgprlemcl  7504  caucvgprprlemcl  7532  suplocsrlempr  7635  lemulge11  8644  nn0ge2m1nn  9057  frecfzennn  10226  reccn2ap  11110  demoivreALT  11507  topcld  12308  metrest  12705  pwle2  13349
 Copyright terms: Public domain W3C validator