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  3321  dfun2  3417  dfin2  3418  0pss  3505  pssv  3507  disj4  3516  zfpair  4228  opabn0  4311  relop  4850  ssrnres  5132  funopab  5303  funcnv2  5325  fnres  5376  dffv2  5608  fnniniseg2  5665  rexsupp  5666  suppss  5674  suppssr  5675  idref  5775  rnoprab  5946  brwitnlem  6522  omeu  6599  elixp  6839  1sdom  7081  dfsup2  7211  dfsup2OLD  7212  wemapso2  7283  card2inf  7285  harndom  7294  dford2  7337  cantnfle  7388  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnfp1  7399  oemapvali  7402  cantnflem1a  7403  cantnflem1c  7405  cantnflem1  7407  tz9.12lem3  7477  dfac4  7765  dfac12a  7790  cflem  7888  cfsmolem  7912  dffin7-2  8040  dfacfin7  8041  brdom3  8169  iunfo  8177  gch3  8318  lbfzo0  10919  gcdcllem3  12708  1nprm  12779  cygctb  15194  rrgsupp  16048  opsrtoslem2  16242  expmhm  16465  expghm  16466  basdif0  16707  txdis1cn  17345  trfil2  17598  txflf  17717  clsnsg  17808  tgpconcomp  17811  perfdvf  19269  wilthlem3  20324  blocnilem  21398  h1de2i  22148  nmop0  22582  nmfn0  22583  lnopconi  22630  lnfnconi  22651  stcltr2i  22871  funcnvmptOLD  23249  funcnvmpt  23250  dftr6  24178  dfpo2  24183  br6  24185  dford5reg  24209  txpss3v  24489  brsset  24500  dfon3  24503  brtxpsd  24505  brtxpsd2  24506  dffun10  24524  elfuns  24525  funpartlem  24552  fullfunfv  24557  dfrdg4  24560  mptelee  24595  hfext  24885  usptoplem  25649  neibastop2lem  26412  compel  27743  dfdfat2  28099
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