Theorem ifpid 1077

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

Assertion

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

Proof of Theorem ifpid

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

Syntax hints:   ↔ wb 205  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 206  df-an 398  df-or 847  df-ifp 1063

This theorem is referenced by:  wl-1mintru2  36370