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 4506. This is essentially pm4.42 1048. (Contributed by BJ, 20-Sep-2019.) |
Ref | Expression |
---|---|
ifpid | ⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifptru 1068 | . 2 ⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)) | |
2 | ifpfal 1069 | . 2 ⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)) | |
3 | 1, 2 | pm2.61i 184 | 1 ⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 if-wif 1057 |
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 209 df-an 399 df-or 844 df-ifp 1058 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |