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

Theorem mpbiran 916
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 504 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 252 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  mpbir2an  918  pm5.63  922  ddif  3563  dfun2  3671  dfin2  3672  0pss  3793  pssv  3795  disj4  3804  zfpair  4612  opabn0  4705  relop  5079  ssrnres  5368  funopab  5542  funcnv2  5568  fnres  5618  dffv2  5860  fnniniseg2OLD  5926  rexsuppOLD  5927  suppssOLD  5935  suppssrOLD  5936  idref  6070  rnoprab  6302  suppssr  6867  brwitnlem  7093  omeu  7170  elixp  7413  1sdom  7657  dfsup2  7835  dfsup2OLD  7836  wemapso2OLD  7910  wemapso2lem  7911  card2inf  7914  harndom  7923  dford2  7969  cantnfp1lem3  8030  cantnfp1  8031  cantnflem1  8039  cantnfleOLD  8051  cantnfp1lem2OLD  8055  cantnfp1lem3OLD  8056  cantnfp1OLD  8057  cantnflem1aOLD  8058  cantnflem1cOLD  8060  cantnflem1OLD  8062  tz9.12lem3  8138  dfac4  8434  dfac12a  8459  cflem  8557  cfsmolem  8581  dffin7-2  8709  dfacfin7  8710  brdom3  8837  iunfo  8845  gch3  8983  lbfzo0  11775  gcdcllem3  14172  1nprm  14243  cygctb  17030  rrgsuppOLD  18072  opsrtoslem2  18281  expmhm  18617  expghm  18645  mat1dimelbas  19077  basdif0  19558  txdis1cn  20240  trfil2  20492  txflf  20611  clsnsg  20712  tgpconcomp  20715  perfdvf  22411  wilthlem3  23480  mptelee  24340  blocnilem  25857  h1de2i  26609  nmop0  27042  nmfn0  27043  lnopconi  27090  lnfnconi  27111  stcltr2i  27331  funcnvmptOLD  27685  funcnvmpt  27686  1stpreima  27702  2ndpreima  27703  suppss3  27730  elmrsubrn  29105  dftr6  29381  dfpo2  29386  br6  29388  dford5reg  29415  txpss3v  29717  brsset  29728  dfon3  29731  brtxpsd  29733  brtxpsd2  29734  dffun10  29753  elfuns  29754  funpartlem  29781  fullfunfv  29786  dfrdg4  29789  dfint3  29791  brub  29793  hfext  30029  neibastop2lem  30380  compel  31551  dfdfat2  32417
  Copyright terms: Public domain W3C validator