![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifpid | Structured version Visualization version GIF version |
Description: Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4571. This is essentially pm4.42 1053. (Contributed by BJ, 20-Sep-2019.) |
Ref | Expression |
---|---|
ifpid | ⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifptru 1074 | . 2 ⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)) | |
2 | ifpfal 1075 | . 2 ⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)) | |
3 | 1, 2 | pm2.61i 182 | 1 ⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 if-wif 1062 |
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 207 df-an 396 df-or 848 df-ifp 1063 |
This theorem is referenced by: wl-1mintru2 37472 |
Copyright terms: Public domain | W3C validator |