Users' Mathboxes Mathbox for Jarvin Udandy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bothfbothsame Structured version   Unicode version

Theorem bothfbothsame 38358
Description: Given both a, b are equivalent to F., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
Hypotheses
Ref Expression
bothfbothsame.1  |-  ( ph  <-> F.  )
bothfbothsame.2  |-  ( ps  <-> F.  )
Assertion
Ref Expression
bothfbothsame  |-  ( ph  <->  ps )

Proof of Theorem bothfbothsame
StepHypRef Expression
1 bothfbothsame.1 . 2  |-  ( ph  <-> F.  )
2 bothfbothsame.2 . 2  |-  ( ps  <-> F.  )
31, 2bitr4i 255 1  |-  ( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   F. wfal 1442
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
This theorem is referenced by:  mdandyv0  38408  mdandyv1  38409  mdandyv2  38410  mdandyv3  38411  mdandyv4  38412  mdandyv5  38413  mdandyv6  38414  mdandyv7  38415  mdandyv8  38416  mdandyv9  38417  mdandyv10  38418  mdandyv11  38419  mdandyv12  38420  mdandyv13  38421  mdandyv14  38422  dandysum2p2e4  38457
  Copyright terms: Public domain W3C validator