Theorem ifpid 1025

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

Assertion

Ref	Expression
ifpid	|- (if- ( ph , ps , ps ) <-> ps )

Proof of Theorem ifpid

Step	Hyp	Ref	Expression
1		ifptru 1023	. 2 |- ( ph -> (if- ( ph , ps , ps ) <-> ps ) )
2		ifpfal 1024	. 2 |- ( -. ph -> (if- ( ph , ps , ps ) <-> ps ) )
3	1, 2	pm2.61i 176	1 |- (if- ( ph , ps , ps ) <-> ps )

Syntax hints:   <-> wb 196  if-wif 1012

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 197  df-or 385  df-an 386  df-ifp 1013

This theorem is referenced by: (None)