Theorem ifpid 1390

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

Assertion

Ref	Expression
ifpid

Proof of Theorem ifpid

Step	Hyp	Ref	Expression
1		ifptru 1388	. 2
2		ifpfal 1389	. 2
3	1, 2	pm2.61i 164	1

Syntax hints:  <->wb 184  if-wif 1380

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 185  df-or 370  df-an 371  df-ifp 1381