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

Theorem jctir 309
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 302 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  311  equvini  1714  funtp  5144  foimacnv  5351  respreima  5514  fpr  5568  dmtpos  6119  ixpsnf1o  6596  ssdomg  6638  exmidfodomrlemim  7021  archnqq  7189  recexgt0sr  7545  ige2m2fzo  9915  climeu  11005  algcvgblem  11626  qredeu  11674  qnumdencoprm  11766  qeqnumdivden  11767  eltg3i  12120  topbas  12131  neipsm  12218  lmbrf  12279  exmidsbthrlem  13028
  Copyright terms: Public domain W3C validator