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

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

Proof of Theorem jctir
StepHypRef Expression
1 jctil.1 . 2  |-  ( ph  ->  ps )
2 jctil.2 . . 3  |-  ch
32a1i 9 . 2  |-  ( ph  ->  ch )
41, 3jca 304 1  |-  ( ph  ->  ( ps  /\  ch ) )
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:  jctr  313  equvini  1745  funtp  5236  foimacnv  5445  respreima  5608  fpr  5662  dmtpos  6216  ixpsnf1o  6694  ssdomg  6736  exmidfodomrlemim  7149  archnqq  7350  recexgt0sr  7706  ige2m2fzo  10124  climeu  11227  algcvgblem  11970  qredeu  12018  qnumdencoprm  12114  qeqnumdivden  12115  eltg3i  12623  topbas  12634  neipsm  12721  lmbrf  12782  exmidsbthrlem  13763
  Copyright terms: Public domain W3C validator