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

Theorem mpbiran 885
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 493 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 244 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  mpbir2an  887  pm5.63  891  ddif  3439  dfun2  3536  dfin2  3537  0pss  3625  pssv  3627  disj4  3636  zfpair  4361  opabn0  4445  relop  4982  ssrnres  5268  funopab  5445  funcnv2  5469  fnres  5520  dffv2  5755  fnniniseg2  5813  rexsupp  5814  suppss  5822  suppssr  5823  idref  5938  rnoprab  6115  brwitnlem  6710  omeu  6787  elixp  7028  1sdom  7270  dfsup2  7405  dfsup2OLD  7406  wemapso2  7477  card2inf  7479  harndom  7488  dford2  7531  cantnfle  7582  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnfp1  7593  oemapvali  7596  cantnflem1a  7597  cantnflem1c  7599  cantnflem1  7601  tz9.12lem3  7671  dfac4  7959  dfac12a  7984  cflem  8082  cfsmolem  8106  dffin7-2  8234  dfacfin7  8235  brdom3  8362  iunfo  8370  gch3  8511  lbfzo0  11125  gcdcllem3  12968  1nprm  13039  cygctb  15456  rrgsupp  16306  opsrtoslem2  16500  expmhm  16731  expghm  16732  basdif0  16973  txdis1cn  17620  trfil2  17872  txflf  17991  clsnsg  18092  tgpconcomp  18095  perfdvf  19743  wilthlem3  20806  blocnilem  22258  h1de2i  23008  nmop0  23442  nmfn0  23443  lnopconi  23490  lnfnconi  23511  stcltr2i  23731  funcnvmptOLD  24035  funcnvmpt  24036  1stpreima  24048  2ndpreima  24049  dftr6  25321  dfpo2  25326  br6  25328  dford5reg  25352  txpss3v  25632  brsset  25643  dfon3  25646  brtxpsd  25648  brtxpsd2  25649  dffun10  25667  elfuns  25668  funpartlem  25695  fullfunfv  25700  dfrdg4  25703  mptelee  25738  hfext  26028  neibastop2lem  26279  compel  27508  dfdfat2  27862
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 178  df-an 361
  Copyright terms: Public domain W3C validator