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

Theorem jctil 308
Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
Hypotheses
Ref Expression
jctil.1  |-  ( ph  ->  ps )
jctil.2  |-  ch
Assertion
Ref Expression
jctil  |-  ( ph  ->  ( ch  /\  ps ) )

Proof of Theorem jctil
StepHypRef Expression
1 jctil.2 . . 3  |-  ch
21a1i 9 . 2  |-  ( ph  ->  ch )
3 jctil.1 . 2  |-  ( ph  ->  ps )
42, 3jca 302 1  |-  ( ph  ->  ( ch  /\  ps ) )
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  310  ddifnel  3175  unidif  3736  iunxdif2  3829  exss  4117  reg2exmidlema  4417  limom  4495  xpiindim  4644  relssres  4825  funco  5131  nfunsn  5421  fliftcnv  5662  fo1stresm  6025  fo2ndresm  6026  dftpos3  6125  tfri1d  6198  rdgtfr  6237  rdgruledefgg  6238  frectfr  6263  elixpsn  6595  mapxpen  6708  phplem2  6713  sbthlem2  6812  sbthlemi3  6813  djuss  6921  caseinl  6942  caseinr  6943  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  nqprrnd  7315  nqprxx  7318  ltexprlempr  7380  recexprlempr  7404  cauappcvgprlemcl  7425  caucvgprlemcl  7448  caucvgprprlemcl  7476  suplocsrlempr  7579  lemulge11  8581  nn0ge2m1nn  8988  frecfzennn  10139  reccn2ap  11022  demoivreALT  11378  topcld  12173  metrest  12570  pwle2  13016
  Copyright terms: Public domain W3C validator