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

Theorem jctir 306
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 300 1  |-  ( ph  ->  ( ps  /\  ch ) )
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:  jctr  308  equvini  1688  funtp  5053  foimacnv  5255  respreima  5411  fpr  5463  dmtpos  6003  ssdomg  6475  exmidfodomrlemim  6806  archnqq  6955  recexgt0sr  7298  ige2m2fzo  9574  climeu  10647  algcvgblem  11111  qredeu  11159  qnumdencoprm  11251  qeqnumdivden  11252  exmidsbthrlem  11556
  Copyright terms: Public domain W3C validator