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  21146  cnprest  23476  cnprest2  23477  cnt0  23533  1stccn  23650  kgencn  23743  qtopcn  23901  fbflim  24163  isflf  24180  cnflf  24189  fclscf  24212  cnfcf  24229  elbl2ps  24576  elbl2  24577  metcn  24730  txmetcn  24735  iscvs  25316  lmclimf  25493  ovolfioo  25656  ovolficc  25657  ovoliun  25694  ismbl2  25716  mbfmulc2lem  25836  mbfmax  25838  mbfposr  25841  mbfaddlem  25849  mbfsup  25853  mbfi1fseqlem4  25907  itg2monolem1  25939  itg2cnlem1  25950  tgellng  28852  isleag  29194  ttgelitv  29262  isspthonpth  30128  clwlkclwwlkflem  30385  clwwlkwwlksb  30435  suppgsumssiun  33416  isfxp  33512  lindflbs  33716  ply1degleel  33909  selvply1rhmlem2  33935  algextdeglem7  34137  ismntoplly  34439  esum2dlem  34506  ntrclselnel1  44816  ntrneicls00  44848  vonvolmbl  47408  dfdfat2  47898  crngprmringidom  49139  ipolubdm  49798  ipoglbdm  49801  isup  49991  functhinc  50259