Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frege52aid Structured version   Unicode version

Theorem frege52aid 36318
Description: The case when the content of  ph is identical with the content of  ps and in which  ph is affirmed and  ps is denied does not take place. Identical to biimp 197. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
frege52aid  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )

Proof of Theorem frege52aid
StepHypRef Expression
1 ax-frege52a 36317 . 2  |-  ( (
ph 
<->  ps )  ->  (if- ( ph , T.  , F.  )  -> if- ( ps , T.  , F.  ) ) )
2 ifpid2 36040 . 2  |-  ( ph  <-> if- (
ph , T.  , F.  ) )
3 ifpid2 36040 . 2  |-  ( ps  <-> if- ( ps , T.  , F.  ) )
41, 2, 33imtr4g 274 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188  if-wif 1421   T. wtru 1439   F. wfal 1443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-frege52a 36317
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ifp 1422  df-tru 1441  df-fal 1444
This theorem is referenced by:  frege53aid  36319  frege57aid  36332  frege75  36398  frege89  36412  frege105  36428
  Copyright terms: Public domain W3C validator