Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > nfded2 | Structured version Visualization version Unicode version |
Description: A deduction theorem that converts a not-free inference directly to deduction form. The first 2 hypotheses are the hypotheses of the deduction form. The third is an equality deduction (e.g. for nfopd 4419) that starts from abidnf 3375. The last is assigned to the inference form (e.g. for nfop 4418) whose hypotheses are satisfied using nfaba1 2770. (Contributed by NM, 19-Nov-2020.) |
Ref | Expression |
---|---|
nfded2.1 | |
nfded2.2 | |
nfded2.3 | |
nfded2.4 |
Ref | Expression |
---|---|
nfded2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfded2.4 | . 2 | |
2 | nfded2.1 | . . 3 | |
3 | nfded2.2 | . . 3 | |
4 | nfnfc1 2767 | . . . . 5 | |
5 | nfnfc1 2767 | . . . . 5 | |
6 | 4, 5 | nfan 1828 | . . . 4 |
7 | nfded2.3 | . . . 4 | |
8 | 6, 7 | nfceqdf 2760 | . . 3 |
9 | 2, 3, 8 | syl2anc 693 | . 2 |
10 | 1, 9 | mpbii 223 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wnfc 2751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-cleq 2615 df-clel 2618 df-nfc 2753 |
This theorem is referenced by: nfopdALT 34258 |
Copyright terms: Public domain | W3C validator |