Theorem mpbiran2 919

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 505	. 2
4	1, 3	bitr4i 252	1

Syntax hints:  <->wb 184  /\wa 369

This theorem is referenced by:  pm5.62  923  reueq  3297  ss0b  3815  eusv1  4646  eusv2nf  4650  eusv2  4651  opthprc  5052  sosn  5074  opelres  5284  fdmrn  5751  f1cnvcnv  5794  fores  5809  f1orn  5831  funfv  5940  dfoprab2  6343  elxp7  6833  tpostpos  6994  dfsup2OLD  7923  canthwe  9050  recmulnq  9363  opelreal  9528  elreal2  9530  eqresr  9535  elnn1uz2  11187  faclbnd4lem1  12371  isprm2  14225  joindm  15633  meetdm  15647  symgbas0  16419  efgs1  16753  funsnfsupOLD  18256  toptopon  19434  ist1-3  19850  perfcls  19866  prdsxmetlem  20871  hhsssh2  26186  choc0  26244  chocnul  26246  shlesb1i  26304  adjeu  26808  isarchi  27726  derang0  28613  nofulllem5  29466  brtxp  29530  brpprod  29535  dfon3  29542  brtxpsd  29544  topmeet  30182  filnetlem2  30197  filnetlem3  30198  fdc  30238  0totbnd  30269  heiborlem3  30309  bj-rabtrALT  34498  bj-snsetex  34521  bj-ifid3g  37710  elintima  37765

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