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  1731  funtp  5176  foimacnv  5385  respreima  5548  fpr  5602  dmtpos  6153  ixpsnf1o  6630  ssdomg  6672  exmidfodomrlemim  7062  archnqq  7237  recexgt0sr  7593  ige2m2fzo  9987  climeu  11077  algcvgblem  11741  qredeu  11789  qnumdencoprm  11882  qeqnumdivden  11883  eltg3i  12239  topbas  12250  neipsm  12337  lmbrf  12398  exmidsbthrlem  13278
 Copyright terms: Public domain W3C validator