Theorem ifpid 1093

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

Assertion

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

Proof of Theorem ifpid

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

This proof depends on syntax axioms:   ↔ wb 209  if-wif 1078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079

This theorem is used by:  wl-1mintru2  38176