MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifpid Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 ifptru 1017 . 2 (𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓))
2 ifpfal 1018 . 2 𝜑 → (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓))
31, 2pm2.61i 175 1 (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓)
Colors of variables: wff setvar class
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)
  Copyright terms: Public domain W3C validator