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

Theorem jctir 313
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 306 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  jctr  315  equvini  1758  funtp  5270  foimacnv  5480  respreima  5645  fpr  5699  dmtpos  6257  ixpsnf1o  6736  ssdomg  6778  exmidfodomrlemim  7200  archnqq  7416  recexgt0sr  7772  ige2m2fzo  10198  climeu  11304  algcvgblem  12049  qredeu  12097  qnumdencoprm  12193  qeqnumdivden  12194  eltg3i  13559  topbas  13570  neipsm  13657  lmbrf  13718  exmidsbthrlem  14773
  Copyright terms: Public domain W3C validator