![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anc2li | Structured version Visualization version 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 552 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-an 378 |
This theorem is referenced by: imdistani 704 pwpw0 4111 sssn 4122 pwsnALT 4185 wfisg 5422 ordtr2 5474 tfis 6700 oeordi 7306 unblem3 7843 trcl 8230 h1datomi 27315 ballotlemfc0 29398 ballotlemfcc 29399 frinsg 30554 dfrdg4 30789 bj-sbsb 31505 sbiota1 36855 |
Copyright terms: Public domain | W3C validator |