Theorem mpbirand 720

Description: Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

Ref	Expression
mpbirand.1	⊢ (𝜑 → 𝜒)
mpbirand.2	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
mpbirand	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem mpbirand

Step	Hyp	Ref	Expression
1		mpbirand.2	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2		mpbirand.1	. . 3 ⊢ (𝜑 → 𝜒)
3	2	biantrurd 542	. 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
4	1, 3	bitr4d 285	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpbiran2d  721  3anibar  1348  rmob2  3849  opbrop  5764  fvdifsupp  8176  wemapso2lem  9524  uzin  12916  supxrre1  13374  ixxun  13406  uzsplit  13643  pfxsuffeqwrdeq  14759  ello12  15593  elo12  15604  fsumss  15802  fprodss  16028  ramval  17093  issect2  17836  ellspsn5b  21153  cnprest  23483  cnprest2  23484  cnt0  23540  1stccn  23657  kgencn  23750  qtopcn  23908  fbflim  24170  isflf  24187  cnflf  24196  fclscf  24219  cnfcf  24236  elbl2ps  24583  elbl2  24584  metcn  24737  txmetcn  24742  iscvs  25323  lmclimf  25500  ovolfioo  25663  ovolficc  25664  ovoliun  25701  ismbl2  25723  mbfmulc2lem  25843  mbfmax  25845  mbfposr  25848  mbfaddlem  25856  mbfsup  25860  mbfi1fseqlem4  25914  itg2monolem1  25946  itg2cnlem1  25957  tgellng  28859  isleag  29201  ttgelitv  29269  isspthonpth  30135  clwlkclwwlkflem  30392  clwwlkwwlksb  30442  suppgsumssiun  33423  isfxp  33519  lindflbs  33723  ply1degleel  33916  selvply1rhmlem2  33942  algextdeglem7  34144  ismntoplly  34446  esum2dlem  34513  ntrclselnel1  44824  ntrneicls00  44856  vonvolmbl  47416  dfdfat2  47906  crngprmringidom  49147  ipolubdm  49806  ipoglbdm  49809  isup  49999  functhinc  50267