![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > anc2li | Unicode version |
Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
Ref | Expression |
---|---|
anc2li.1 |
Ref | Expression |
---|---|
anc2li |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anc2li.1 | . 2 | |
2 | id 22 | . 2 | |
3 | 1, 2 | jctild 543 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 /\ wa 369 |
This theorem is referenced by: imdistani 690 pwpw0 4178 sssn 4188 pwsnALT 4244 ordtr2 4927 tfis 6689 oeordi 7255 unblem3 7794 trcl 8180 h1datomi 26499 ballotlemfc0 28431 ballotlemfcc 28432 wfisg 29289 frinsg 29325 dfrdg4 29600 sbiota1 31341 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 185 df-an 371 |
Copyright terms: Public domain | W3C validator |