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

Theorem mpbiran 916
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 506 . 2  |-  ( ch  <->  ( ps  /\  ch )
)
41, 3bitr4i 252 1  |-  ( ph  <->  ch )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  mpbir2an  918  pm5.63  922  ddif  3636  dfun2  3733  dfin2  3734  0pss  3864  pssv  3866  disj4  3875  zfpair  4684  opabn0  4778  relop  5151  ssrnres  5443  funopab  5619  funcnv2  5645  fnres  5695  dffv2  5938  fnniniseg2OLD  6003  rexsuppOLD  6004  suppssOLD  6012  suppssrOLD  6013  idref  6139  rnoprab  6367  suppssr  6928  brwitnlem  7154  omeu  7231  elixp  7473  1sdom  7719  dfsup2  7898  dfsup2OLD  7899  wemapso2OLD  7973  wemapso2lem  7974  card2inf  7977  harndom  7986  dford2  8033  cantnfp1lem3  8095  cantnfp1  8096  cantnflem1  8104  cantnfleOLD  8116  cantnfp1lem2OLD  8120  cantnfp1lem3OLD  8121  cantnfp1OLD  8122  cantnflem1aOLD  8123  cantnflem1cOLD  8125  cantnflem1OLD  8127  tz9.12lem3  8203  dfac4  8499  dfac12a  8524  cflem  8622  cfsmolem  8646  dffin7-2  8774  dfacfin7  8775  brdom3  8902  iunfo  8910  gch3  9050  lbfzo0  11826  gcdcllem3  14006  1nprm  14077  cygctb  16685  rrgsuppOLD  17711  opsrtoslem2  17920  expmhm  18253  expghm  18296  expghmOLD  18297  mat1dimelbas  18740  basdif0  19221  txdis1cn  19871  trfil2  20123  txflf  20242  clsnsg  20343  tgpconcomp  20346  perfdvf  22042  wilthlem3  23072  mptelee  23874  blocnilem  25395  h1de2i  26147  nmop0  26581  nmfn0  26582  lnopconi  26629  lnfnconi  26650  stcltr2i  26870  funcnvmptOLD  27181  funcnvmpt  27182  1stpreima  27196  2ndpreima  27197  suppss3  27222  dftr6  28756  dfpo2  28761  br6  28763  dford5reg  28791  txpss3v  29105  brsset  29116  dfon3  29119  brtxpsd  29121  brtxpsd2  29122  dffun10  29141  elfuns  29142  funpartlem  29169  fullfunfv  29174  dfrdg4  29177  dfint3  29179  brub  29181  hfext  29417  neibastop2lem  29781  compel  30925  dfdfat2  31683
  Copyright terms: Public domain W3C validator