Theorem mpbiran2 992

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)

Hypotheses

Ref	Expression
mpbiran2.1	⊢ 𝜒
mpbiran2.2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbiran2	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem mpbiran2

Step	Hyp	Ref	Expression
1		mpbiran2.2	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		mpbiran2.1	. . 3 ⊢ 𝜒
3	2	biantru 527	. 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜒))
4	1, 3	bitr4i 267	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pm5.62  996  reueq  3537  ss0b  4108  eusv1  5001  eusv2nf  5005  eusv2  5006  opthprc  5316  sosn  5337  opelresOLD  5553  fdmrn  6217  f1cnvcnv  6262  fores  6277  f1orn  6300  funfv  6419  dfoprab2  6858  elxp7  7360  tpostpos  7533  canthwe  9657  recmulnq  9970  opelreal  10135  elreal2  10137  eqresr  10142  elnn1uz2  11950  faclbnd4lem1  13266  isprm2  15589  joindm  17196  meetdm  17210  symgbas0  18006  efgs1  18340  toptopon  20916  ist1-3  21347  perfcls  21363  prdsxmetlem  22366  rusgrprc  26688  hhsssh2  28428  choc0  28486  chocnul  28488  shlesb1i  28546  adjeu  29049  isarchi  30037  derang0  31450  brtxp  32285  brpprod  32290  dfon3  32297  brtxpsd  32299  topmeet  32657  filnetlem2  32672  filnetlem3  32673  bj-rabtrALT  33225  bj-snsetex  33249  relowlpssretop  33515  poimirlem28  33742  fdc  33846  0totbnd  33877  heiborlem3  33917  cossssid  34532  cnvrefrelcoss2  34598  ifpid3g  38331  elintima  38439