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

Theorem ifpid 1433
Description: Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 3952. This is essentially pm4.42 968. (Contributed by BJ, 20-Sep-2019.)
Assertion
Ref Expression
ifpid  |-  (if- (
ph ,  ps ,  ps )  <->  ps )

Proof of Theorem ifpid
StepHypRef Expression
1 ifptru 1431 . 2  |-  ( ph  ->  (if- ( ph ,  ps ,  ps )  <->  ps ) )
2 ifpfal 1432 . 2  |-  ( -. 
ph  ->  (if- ( ph ,  ps ,  ps )  <->  ps ) )
31, 2pm2.61i 167 1  |-  (if- (
ph ,  ps ,  ps )  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187  if-wif 1420
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 188  df-or 371  df-an 372  df-ifp 1421
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator