Theorem ifpid 1073

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

Assertion

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

Proof of Theorem ifpid

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

Syntax hints:   ↔ wb 209  if-wif 1058

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 210  df-an 400  df-or 845  df-ifp 1059

This theorem is referenced by:  wl-1mintru2  35208