Description: Bound-variable hypothesis builder for a conditional operator. (Contributed by NM, 16-Feb-2005) (Proof shortened by Andrew Salmon, 26-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfif.1 | |- F/ x ph |
|
| nfif.2 | |- F/_ x A |
||
| nfif.3 | |- F/_ x B |
||
| Assertion | nfif | |- F/_ x if ( ph , A , B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfif.1 | |- F/ x ph |
|
| 2 | nfif.2 | |- F/_ x A |
|
| 3 | nfif.3 | |- F/_ x B |
|
| 4 | 1 | a1i | |- ( T. -> F/ x ph ) |
| 5 | 2 | a1i | |- ( T. -> F/_ x A ) |
| 6 | 3 | a1i | |- ( T. -> F/_ x B ) |
| 7 | 4 5 6 | nfifd | |- ( T. -> F/_ x if ( ph , A , B ) ) |
| 8 | 7 | mptru | |- F/_ x if ( ph , A , B ) |