ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jctil Unicode 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  |-  ( 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 300 1  |-  ( ph  ->  ( ch  /\  ps ) )
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  3104  unidif  3641  iunxdif2  3734  exss  3990  reg2exmidlema  4285  limom  4362  xpiindim  4501  relssres  4676  funco  4970  nfunsn  5239  fliftcnv  5466  fo1stresm  5819  fo2ndresm  5820  dftpos3  5911  tfri1d  5984  rdgtfr  6023  rdgruledefgg  6024  frectfr  6049  phplem2  6388  nqprrnd  6795  nqprxx  6798  ltexprlempr  6860  recexprlempr  6884  cauappcvgprlemcl  6905  caucvgprlemcl  6928  caucvgprprlemcl  6956  lemulge11  8011  nn0ge2m1nn  8415  frecfzennn  9508
  Copyright terms: Public domain W3C validator