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

Step	Hyp	Ref	Expression
1		mpbiran.2	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		mpbiran.1	. . 3 ⊢ 𝜓
3	2	biantrur 530	. 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 277	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  mpbiran2  706  mpbir2an  707  pm5.63  1016  equsexALT  2419  velcomp  3898  ddif  4067  dfun2  4190  dfin2  4191  0pss  4375  pssv  4377  disj4  4389  pwpwab  5028  zfpair  5339  opabn0  5459  relop  5748  ssrnres  6070  funopab  6453  funcnv2  6486  fnres  6543  dffv2  6845  idref  7000  rnoprab  7356  suppssr  7983  frrlem9  8081  brwitnlem  8299  omeu  8378  elixp  8650  1sdom  8955  dfsup2  9133  card2inf  9244  harndom  9251  dford2  9308  cantnfp1lem3  9368  cantnfp1  9369  cantnflem1  9377  tz9.12lem3  9478  djulf1o  9601  djurf1o  9602  dfac4  9809  dfac12a  9835  cflem  9933  cfsmolem  9957  dffin7-2  10085  dfacfin7  10086  brdom3  10215  iunfo  10226  gch3  10363  lbfzo0  13355  gcdcllem3  16136  1nprm  16312  cygctb  19408  expmhm  20579  expghm  20609  opsrtoslem2  21173  mat1dimelbas  21528  basdif0  22011  txdis1cn  22694  trfil2  22946  txflf  23065  clsnsg  23169  tgpconncomp  23172  perfdvf  24972  wilthlem3  26124  mptelee  27166  iscplgr  27685  rgrprcx  27862  blocnilem  29067  h1de2i  29816  nmop0  30249  nmfn0  30250  lnopconi  30297  lnfnconi  30318  stcltr2i  30538  funcnvmpt  30906  1stpreima  30941  2ndpreima  30942  suppss3  30961  fmla0  33244  fmlasuc0  33246  elmrsubrn  33382  dftr6  33624  br6  33630  dford5reg  33664  ttrclresv  33703  naddcllem  33758  noeta2  33906  etasslt2  33935  made0  33984  txpss3v  34107  brtxp  34109  brpprod  34114  brsset  34118  dfon3  34121  brtxpsd  34123  brtxpsd2  34124  dffun10  34143  elfuns  34144  funpartlem  34171  fullfunfv  34176  dfrdg4  34180  dfint3  34181  brub  34183  hfext  34412  neibastop2lem  34476  bj-equsexval  34768  bj-elid3  35265  finxp0  35489  finxp1o  35490  brvdif  36327  xrnss3v  36429  ntrneiel2  41585  ntrneik4w  41599  ismnushort  41808  funressnvmo  44426  dfdfat2  44507