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

Theorem mpbiran 708
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 534 . 2 (𝜒 ↔ (𝜓𝜒))
41, 3bitr4i 281 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  mpbiran2  709  mpbir2an  710  pm5.63  1017  equsexvwOLD  2013  equsexv  2270  equsexALT  2442  velcomp  3925  ddif  4089  dfun2  4211  dfin2  4212  0pss  4369  pssv  4371  disj4  4381  pwpwab  4998  zfpair  5295  opabn0  5413  relop  5694  ssrnres  6008  funopab  6363  funcnv2  6395  fnres  6447  dffv2  6729  idref  6881  rnoprab  7231  suppssr  7836  brwitnlem  8107  omeu  8186  elixp  8443  1sdom  8697  dfsup2  8884  card2inf  8995  harndom  9002  dford2  9059  cantnfp1lem3  9119  cantnfp1  9120  cantnflem1  9128  tz9.12lem3  9194  djulf1o  9317  djurf1o  9318  dfac4  9525  dfac12a  9551  cflem  9645  cfsmolem  9669  dffin7-2  9797  dfacfin7  9798  brdom3  9927  iunfo  9938  gch3  10075  lbfzo0  13060  gcdcllem3  15827  1nprm  16000  cygctb  18991  opsrtoslem2  20241  expmhm  20590  expghm  20619  mat1dimelbas  21056  basdif0  21537  txdis1cn  22219  trfil2  22471  txflf  22590  clsnsg  22694  tgpconncomp  22697  perfdvf  24485  wilthlem3  25634  mptelee  26668  iscplgr  27184  rgrprcx  27361  blocnilem  28566  h1de2i  29315  nmop0  29748  nmfn0  29749  lnopconi  29796  lnfnconi  29817  stcltr2i  30037  funcnvmpt  30399  1stpreima  30429  2ndpreima  30430  suppss3  30447  fmla0  32637  fmlasuc0  32639  elmrsubrn  32775  dftr6  32994  br6  33001  dford5reg  33035  frrlem9  33139  txpss3v  33347  brtxp  33349  brpprod  33354  brsset  33358  dfon3  33361  brtxpsd  33363  brtxpsd2  33364  dffun10  33383  elfuns  33384  funpartlem  33411  fullfunfv  33416  dfrdg4  33420  dfint3  33421  brub  33423  hfext  33652  neibastop2lem  33716  bj-equsexval  34001  bj-elid3  34477  finxp0  34696  finxp1o  34697  brvdif  35568  xrnss3v  35670  ntrneiel2  40603  ntrneik4w  40617  funressnvmo  43460  dfdfat2  43507
  Copyright terms: Public domain W3C validator