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

Theorem mpbiran 884
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 492 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 243 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  mpbir2an  886  pm5.63  890  ddif  3308  dfun2  3404  dfin2  3405  0pss  3492  pssv  3494  disj4  3503  zfpair  4212  opabn0  4295  relop  4834  ssrnres  5116  funopab  5287  funcnv2  5309  fnres  5360  dffv2  5592  fnniniseg2  5649  rexsupp  5650  suppss  5658  suppssr  5659  idref  5759  rnoprab  5930  brwitnlem  6506  omeu  6583  elixp  6823  1sdom  7065  dfsup2  7195  dfsup2OLD  7196  wemapso2  7267  card2inf  7269  harndom  7278  dford2  7321  cantnfle  7372  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnfp1  7383  oemapvali  7386  cantnflem1a  7387  cantnflem1c  7389  cantnflem1  7391  tz9.12lem3  7461  dfac4  7749  dfac12a  7774  cflem  7872  cfsmolem  7896  dffin7-2  8024  dfacfin7  8025  brdom3  8153  iunfo  8161  gch3  8302  lbfzo0  10903  gcdcllem3  12692  1nprm  12763  cygctb  15178  rrgsupp  16032  opsrtoslem2  16226  expmhm  16449  expghm  16450  basdif0  16691  txdis1cn  17329  trfil2  17582  txflf  17701  clsnsg  17792  tgpconcomp  17795  perfdvf  19253  wilthlem3  20308  blocnilem  21382  h1de2i  22132  nmop0  22566  nmfn0  22567  lnopconi  22614  lnfnconi  22635  stcltr2i  22855  funcnvmptOLD  23234  funcnvmpt  23235  dftr6  24107  dfpo2  24112  br6  24114  dford5reg  24138  txpss3v  24418  brsset  24429  dfon3  24432  brtxpsd  24434  brtxpsd2  24435  dffun10  24453  elfuns  24454  funpartfun  24481  fullfunfv  24485  dfrdg4  24488  mptelee  24523  hfext  24813  usptoplem  25546  neibastop2lem  26309  compel  27640  dfdfat2  27994
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator