ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancld Structured version   Unicode 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  6565  1idpru  6566  msqge0  7380  mulge0  7383  fzospliti  8782
  Copyright terms: Public domain W3C validator