Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ancld | Unicode version |
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.) |
Ref | Expression |
---|---|
ancld.1 |
Ref | Expression |
---|---|
ancld |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 21 | . 2 | |
2 | ancld.1 | . 2 | |
3 | 1, 2 | jcad 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 1983 cgsexg 2589 cgsex2g 2590 cgsex4g 2591 reximdva0m 3236 difsn 3501 preq12b 3541 elres 4646 relssres 4648 fnoprabg 5602 1idprl 6688 1idpru 6689 msqge0 7607 mulge0 7610 fzospliti 9032 sqrt2irr 9878 ialgcvga 9890 |
Copyright terms: Public domain | W3C validator |