ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jctir GIF 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 (𝜑𝜓)
jctil.2 𝜒
Assertion
Ref Expression
jctir (𝜑 → (𝜓𝜒))

Proof of Theorem jctir
StepHypRef Expression
1 jctil.1 . 2 (𝜑𝜓)
2 jctil.2 . . 3 𝜒
32a1i 9 . 2 (𝜑𝜒)
41, 3jca 304 1 (𝜑 → (𝜓𝜒))
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  1716  funtp  5146  foimacnv  5353  respreima  5516  fpr  5570  dmtpos  6121  ixpsnf1o  6598  ssdomg  6640  exmidfodomrlemim  7025  archnqq  7193  recexgt0sr  7549  ige2m2fzo  9943  climeu  11033  algcvgblem  11657  qredeu  11705  qnumdencoprm  11798  qeqnumdivden  11799  eltg3i  12152  topbas  12163  neipsm  12250  lmbrf  12311  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator