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

Theorem mpbiran 886
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 494 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 245 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  mpbir2an  888  pm5.63  892  ddif  3480  dfun2  3577  dfin2  3578  0pss  3666  pssv  3668  disj4  3677  zfpair  4402  opabn0  4486  relop  5024  ssrnres  5310  funopab  5487  funcnv2  5511  fnres  5562  dffv2  5797  fnniniseg2  5855  rexsupp  5856  suppss  5864  suppssr  5865  idref  5980  rnoprab  6157  brwitnlem  6752  omeu  6829  elixp  7070  1sdom  7312  dfsup2  7448  dfsup2OLD  7449  wemapso2  7522  card2inf  7524  harndom  7533  dford2  7576  cantnfle  7627  cantnfp1lem2  7636  cantnfp1lem3  7637  cantnfp1  7638  oemapvali  7641  cantnflem1a  7642  cantnflem1c  7644  cantnflem1  7646  tz9.12lem3  7716  dfac4  8004  dfac12a  8029  cflem  8127  cfsmolem  8151  dffin7-2  8279  dfacfin7  8280  brdom3  8407  iunfo  8415  gch3  8556  lbfzo0  11171  gcdcllem3  13014  1nprm  13085  cygctb  15502  rrgsupp  16352  opsrtoslem2  16546  expmhm  16777  expghm  16778  basdif0  17019  txdis1cn  17668  trfil2  17920  txflf  18039  clsnsg  18140  tgpconcomp  18143  perfdvf  19791  wilthlem3  20854  blocnilem  22306  h1de2i  23056  nmop0  23490  nmfn0  23491  lnopconi  23538  lnfnconi  23559  stcltr2i  23779  funcnvmptOLD  24083  funcnvmpt  24084  1stpreima  24096  2ndpreima  24097  dftr6  25374  dfpo2  25379  br6  25381  dford5reg  25410  txpss3v  25724  brsset  25735  dfon3  25738  brtxpsd  25740  brtxpsd2  25741  dffun10  25760  elfuns  25761  funpartlem  25788  fullfunfv  25793  dfrdg4  25796  dfint3  25798  brub  25800  mptelee  25835  hfext  26125  neibastop2lem  26390  compel  27618  dfdfat2  27972
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 179  df-an 362
  Copyright terms: Public domain W3C validator