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

Theorem jctil 299
 Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
Hypotheses
Ref Expression
jctil.1 (𝜑𝜓)
jctil.2 𝜒
Assertion
Ref Expression
jctil (𝜑 → (𝜒𝜓))

Proof of Theorem jctil
StepHypRef Expression
1 jctil.2 . . 3 𝜒
21a1i 9 . 2 (𝜑𝜒)
3 jctil.1 . 2 (𝜑𝜓)
42, 3jca 294 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105 This theorem is referenced by:  jctl  301  ddifnel  3102  unidif  3639  iunxdif2  3732  exss  3990  reg2exmidlema  4286  onpsssuc  4322  limom  4363  xpiindim  4500  relssres  4675  funco  4967  nfunsn  5234  fliftcnv  5462  fo1stresm  5815  fo2ndresm  5816  dftpos3  5907  tfri1d  5979  rdgtfr  5991  rdgruledefgg  5992  frectfr  6015  phplem2  6346  nqprrnd  6698  nqprxx  6701  ltexprlempr  6763  recexprlempr  6787  cauappcvgprlemcl  6808  caucvgprlemcl  6831  caucvgprprlemcl  6859  lemulge11  7906  nn0ge2m1nn  8298  frecfzennn  9366
 Copyright terms: Public domain W3C validator