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

Theorem jctil 305
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 300 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  jctl  307  ddifnel  3131  unidif  3685  iunxdif2  3778  exss  4054  reg2exmidlema  4350  limom  4428  xpiindim  4573  relssres  4750  funco  5054  nfunsn  5338  fliftcnv  5574  fo1stresm  5932  fo2ndresm  5933  dftpos3  6027  tfri1d  6100  rdgtfr  6139  rdgruledefgg  6140  frectfr  6165  mapxpen  6564  phplem2  6569  sbthlem2  6667  sbthlemi3  6668  djuss  6761  exmidfodomrlemr  6828  exmidfodomrlemrALT  6829  nqprrnd  7102  nqprxx  7105  ltexprlempr  7167  recexprlempr  7191  cauappcvgprlemcl  7212  caucvgprlemcl  7235  caucvgprprlemcl  7263  lemulge11  8327  nn0ge2m1nn  8733  frecfzennn  9833  demoivreALT  11063
  Copyright terms: Public domain W3C validator