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

Theorem mpbiran 932
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 514 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 260 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  mpbir2an  934  pm5.63  938  equsexvw  1856  equsexv  2085  equsexALT  2144  ddif  3554  dfun2  3669  dfin2  3670  0pss  3806  pssv  3808  disj4  3817  zfpair  4637  opabn0  4732  relop  4990  ssrnres  5281  funopab  5622  funcnv2  5652  fnres  5702  dffv2  5953  idref  6164  rnoprab  6398  suppssr  6965  brwitnlem  7227  omeu  7304  elixp  7547  1sdom  7793  dfsup2  7976  wemapso2lem  8085  card2inf  8088  harndom  8097  dford2  8143  cantnfp1lem3  8203  cantnfp1  8204  cantnflem1  8212  tz9.12lem3  8278  dfac4  8571  dfac12a  8596  cflem  8694  cfsmolem  8718  dffin7-2  8846  dfacfin7  8847  brdom3  8974  iunfo  8982  gch3  9119  lbfzo0  11983  gcdcllem3  14554  1nprm  14708  cygctb  17604  opsrtoslem2  18785  expmhm  19113  expghm  19144  mat1dimelbas  19573  basdif0  20045  txdis1cn  20727  trfil2  20980  txflf  21099  clsnsg  21202  tgpconcomp  21205  perfdvf  22937  wilthlem3  24074  mptelee  25004  blocnilem  26526  h1de2i  27287  nmop0  27720  nmfn0  27721  lnopconi  27768  lnfnconi  27789  stcltr2i  28009  funcnvmptOLD  28345  funcnvmpt  28346  1stpreima  28362  2ndpreima  28363  suppss3  28387  elmrsubrn  30230  dftr6  30461  dfpo2  30466  br6  30468  dford5reg  30499  txpss3v  30716  brsset  30727  dfon3  30730  brtxpsd  30732  brtxpsd2  30733  dffun10  30752  elfuns  30753  funpartlem  30780  fullfunfv  30785  dfrdg4  30789  dfint3  30790  brub  30792  hfext  31021  neibastop2lem  31087  bj-equsexval  31315  finxp0  31853  finxp1o  31854  compel  36861  dfdfat2  38778  rgrprcx  39796
  Copyright terms: Public domain W3C validator