Theorem ifpid 1019

Description: Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4075. This is essentially pm4.42 995. (Contributed by BJ, 20-Sep-2019.)

Assertion

Ref	Expression
ifpid	⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)

Proof of Theorem ifpid

Step	Hyp	Ref	Expression
1		ifptru 1017	. 2 ⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓))
2		ifpfal 1018	. 2 ⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓))
3	1, 2	pm2.61i 175	1 ⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)

Syntax hints:   ↔ wb 195  if-wif 1006

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 196  df-or 384  df-an 385  df-ifp 1007

This theorem is referenced by: (None)