ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jctir GIF 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 (𝜑𝜓)
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 300 1 (𝜑 → (𝜓𝜒))
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  1685  funtp  5023  foimacnv  5222  respreima  5375  fpr  5424  dmtpos  5956  ssdomg  6428  exmidfodomrlemim  6748  archnqq  6897  recexgt0sr  7240  ige2m2fzo  9512  climeu  10523  algcvgblem  10825  qredeu  10873  qnumdencoprm  10965  qeqnumdivden  10966  exmidsbthrlem  11268
  Copyright terms: Public domain W3C validator