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

Theorem ancld 308
Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
Hypothesis
Ref Expression
ancld.1 (φ → (ψχ))
Assertion
Ref Expression
ancld (φ → (ψ → (ψ χ)))

Proof of Theorem ancld
StepHypRef Expression
1 idd 21 . 2 (φ → (ψψ))
2 ancld.1 . 2 (φ → (ψχ))
31, 2jcad 291 1 (φ → (ψ → (ψ χ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  mopick2  1980  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  reximdva0m  3230  difsn  3492  preq12b  3532  elres  4589  relssres  4591  fnoprabg  5544  1idprl  6564  1idpru  6565  msqge0  7360  mulge0  7363  fzospliti  8762
  Copyright terms: Public domain W3C validator