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

Theorem mpbiran 705
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 531 . 2 (𝜒 ↔ (𝜓𝜒))
41, 3bitr4i 279 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  mpbiran2  706  mpbir2an  707  pm5.63  1013  equsexvwOLD  2003  equsexv  2259  equsexALT  2432  velcomp  3948  ddif  4110  dfun2  4233  dfin2  4234  0pss  4392  pssv  4394  disj4  4404  pwpwab  5016  zfpair  5312  opabn0  5431  relop  5714  ssrnres  6028  funopab  6383  funcnv2  6415  fnres  6467  dffv2  6749  idref  6900  rnoprab  7246  suppssr  7850  brwitnlem  8121  omeu  8200  elixp  8456  1sdom  8709  dfsup2  8896  card2inf  9007  harndom  9016  dford2  9071  cantnfp1lem3  9131  cantnfp1  9132  cantnflem1  9140  tz9.12lem3  9206  djulf1o  9329  djurf1o  9330  dfac4  9536  dfac12a  9562  cflem  9656  cfsmolem  9680  dffin7-2  9808  dfacfin7  9809  brdom3  9938  iunfo  9949  gch3  10086  lbfzo0  13065  gcdcllem3  15838  1nprm  16011  cygctb  18941  opsrtoslem2  20193  expmhm  20542  expghm  20571  mat1dimelbas  21008  basdif0  21489  txdis1cn  22171  trfil2  22423  txflf  22542  clsnsg  22645  tgpconncomp  22648  perfdvf  24428  wilthlem3  25574  mptelee  26608  iscplgr  27124  rgrprcx  27301  blocnilem  28508  h1de2i  29257  nmop0  29690  nmfn0  29691  lnopconi  29738  lnfnconi  29759  stcltr2i  29979  funcnvmpt  30340  1stpreima  30368  2ndpreima  30369  suppss3  30386  fmla0  32526  fmlasuc0  32528  elmrsubrn  32664  dftr6  32883  br6  32890  dford5reg  32924  frrlem9  33028  txpss3v  33236  brtxp  33238  brpprod  33243  brsset  33247  dfon3  33250  brtxpsd  33252  brtxpsd2  33253  dffun10  33272  elfuns  33273  funpartlem  33300  fullfunfv  33305  dfrdg4  33309  dfint3  33310  brub  33312  hfext  33541  neibastop2lem  33605  bj-equsexval  33890  bj-elid3  34351  finxp0  34554  finxp1o  34555  brvdif  35403  xrnss3v  35504  ntrneiel2  40314  ntrneik4w  40328  funressnvmo  43157  dfdfat2  43204
  Copyright terms: Public domain W3C validator