Description: Inference associated with iffalse . (Contributed by BJ, 7-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | iffalsei.1 | |- -. ph |
|
| Assertion | iffalsei | |- if ( ph , A , B ) = B |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iffalsei.1 | |- -. ph |
|
| 2 | iffalse | |- ( -. ph -> if ( ph , A , B ) = B ) |
|
| 3 | 1 2 | ax-mp | |- if ( ph , A , B ) = B |