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

Theorem mpbiran 918
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
Hypotheses
Ref Expression
mpbiran.1
mpbiran.2
Assertion
Ref Expression
mpbiran

Proof of Theorem mpbiran
StepHypRef Expression
1 mpbiran.2 . 2
2 mpbiran.1 . . 3
32biantrur 506 . 2
41, 3bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  mpbir2an  920  pm5.63  924  ddif  3635  dfun2  3732  dfin2  3733  0pss  3864  pssv  3866  disj4  3875  zfpair  4689  opabn0  4783  relop  5158  ssrnres  5450  funopab  5626  funcnv2  5652  fnres  5702  dffv2  5946  fnniniseg2OLD  6011  rexsuppOLD  6012  suppssOLD  6020  suppssrOLD  6021  idref  6153  rnoprab  6385  suppssr  6950  brwitnlem  7176  omeu  7253  elixp  7496  1sdom  7742  dfsup2  7922  dfsup2OLD  7923  wemapso2OLD  7998  wemapso2lem  7999  card2inf  8002  harndom  8011  dford2  8058  cantnfp1lem3  8120  cantnfp1  8121  cantnflem1  8129  cantnfleOLD  8141  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  cantnflem1aOLD  8148  cantnflem1cOLD  8150  cantnflem1OLD  8152  tz9.12lem3  8228  dfac4  8524  dfac12a  8549  cflem  8647  cfsmolem  8671  dffin7-2  8799  dfacfin7  8800  brdom3  8927  iunfo  8935  gch3  9075  lbfzo0  11862  gcdcllem3  14151  1nprm  14222  cygctb  16894  rrgsuppOLD  17940  opsrtoslem2  18149  expmhm  18485  expghm  18529  expghmOLD  18530  mat1dimelbas  18973  basdif0  19454  txdis1cn  20136  trfil2  20388  txflf  20507  clsnsg  20608  tgpconcomp  20611  perfdvf  22307  wilthlem3  23344  mptelee  24198  blocnilem  25719  h1de2i  26471  nmop0  26905  nmfn0  26906  lnopconi  26953  lnfnconi  26974  stcltr2i  27194  funcnvmptOLD  27509  funcnvmpt  27510  1stpreima  27524  2ndpreima  27525  suppss3  27550  elmrsubrn  28880  dftr6  29179  dfpo2  29184  br6  29186  dford5reg  29214  txpss3v  29528  brsset  29539  dfon3  29542  brtxpsd  29544  brtxpsd2  29545  dffun10  29564  elfuns  29565  funpartlem  29592  fullfunfv  29597  dfrdg4  29600  dfint3  29602  brub  29604  hfext  29840  neibastop2lem  30178  compel  31347  dfdfat2  32216
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
  Copyright terms: Public domain W3C validator