Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imim3i | Unicode version |
Description: Inference adding three nested antecedents. (Contributed by NM, 19-Dec-2006.) |
Ref | Expression |
---|---|
imim3i.1 |
Ref | Expression |
---|---|
imim3i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim3i.1 | . . 3 | |
2 | 1 | imim2i 14 | . 2 |
3 | 2 | a2d 26 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 |
This theorem is referenced by: pm2.83 77 pm5.74 244 bi3antOLD 289 pm3.43i 456 ral2imi 2845 ceqsalt 3132 pm10.57 31276 ee33 33291 bj-bi3ant 34178 bj-ceqsalt0 34449 bj-ceqsalt1 34450 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
Copyright terms: Public domain | W3C validator |