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  5269  foimacnv  5479  respreima  5644  fpr  5698  dmtpos  6256  ixpsnf1o  6735  ssdomg  6777  exmidfodomrlemim  7199  archnqq  7415  recexgt0sr  7771  ige2m2fzo  10197  climeu  11303  algcvgblem  12048  qredeu  12096  qnumdencoprm  12192  qeqnumdivden  12193  eltg3i  13526  topbas  13537  neipsm  13624  lmbrf  13685  exmidsbthrlem  14740
  Copyright terms: Public domain W3C validator