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

Theorem mpbiran 909
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
Hypotheses
Ref Expression
mpbiran.1  |-  ps
mpbiran.2  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbiran  |-  ( ph  <->  ch )

Proof of Theorem mpbiran
StepHypRef Expression
1 mpbiran.2 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
2 mpbiran.1 . . 3  |-  ps
32biantrur 506 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 252 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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-an 371
This theorem is referenced by:  mpbir2an  911  pm5.63  915  ddif  3589  dfun2  3686  dfin2  3687  0pss  3817  pssv  3819  disj4  3828  zfpair  4630  opabn0  4720  relop  5091  ssrnres  5377  funopab  5552  funcnv2  5578  fnres  5628  dffv2  5866  fnniniseg2OLD  5929  rexsuppOLD  5930  suppssOLD  5938  suppssrOLD  5939  idref  6060  rnoprab  6276  suppssr  6823  brwitnlem  7050  omeu  7127  elixp  7373  1sdom  7619  dfsup2  7796  dfsup2OLD  7797  wemapso2OLD  7870  wemapso2lem  7871  card2inf  7874  harndom  7883  dford2  7930  cantnfp1lem3  7992  cantnfp1  7993  cantnflem1  8001  cantnfleOLD  8013  cantnfp1lem2OLD  8017  cantnfp1lem3OLD  8018  cantnfp1OLD  8019  cantnflem1aOLD  8020  cantnflem1cOLD  8022  cantnflem1OLD  8024  tz9.12lem3  8100  dfac4  8396  dfac12a  8421  cflem  8519  cfsmolem  8543  dffin7-2  8671  dfacfin7  8672  brdom3  8799  iunfo  8807  gch3  8947  lbfzo0  11696  gcdcllem3  13808  1nprm  13879  cygctb  16481  rrgsuppOLD  17478  opsrtoslem2  17682  expmhm  17998  expghm  18041  expghmOLD  18042  basdif0  18683  txdis1cn  19333  trfil2  19585  txflf  19704  clsnsg  19805  tgpconcomp  19808  perfdvf  21504  wilthlem3  22534  mptelee  23286  blocnilem  24349  h1de2i  25101  nmop0  25535  nmfn0  25536  lnopconi  25583  lnfnconi  25604  stcltr2i  25824  funcnvmptOLD  26130  funcnvmpt  26131  1stpreima  26145  2ndpreima  26146  suppss3  26171  dftr6  27697  dfpo2  27702  br6  27704  dford5reg  27732  txpss3v  28046  brsset  28057  dfon3  28060  brtxpsd  28062  brtxpsd2  28063  dffun10  28082  elfuns  28083  funpartlem  28110  fullfunfv  28115  dfrdg4  28118  dfint3  28120  brub  28122  hfext  28358  neibastop2lem  28722  compel  29835  dfdfat2  30178  mat1dimelbas  31024
  Copyright terms: Public domain W3C validator