Theorem mpbirand 707

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 532	. 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
4	1, 3	bitr4d 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  mpbiran2d  708  3anibar  1330  rmob2  3841  opbrop  5712  fvdifsupp  8096  wemapso2lem  9433  uzin  12764  supxrre1  13221  ixxun  13253  uzsplit  13488  pfxsuffeqwrdeq  14597  ello12  15415  elo12  15426  fsumss  15624  fprodss  15847  ramval  16912  issect2  17653  ellspsn5b  20921  cnprest  23197  cnprest2  23198  cnt0  23254  1stccn  23371  kgencn  23464  qtopcn  23622  fbflim  23884  isflf  23901  cnflf  23910  fclscf  23933  cnfcf  23950  elbl2ps  24297  elbl2  24298  metcn  24451  txmetcn  24456  iscvs  25047  lmclimf  25224  ovolfioo  25388  ovolficc  25389  ovoliun  25426  ismbl2  25448  mbfmulc2lem  25568  mbfmax  25570  mbfposr  25573  mbfaddlem  25581  mbfsup  25585  mbfi1fseqlem4  25639  itg2monolem1  25671  itg2cnlem1  25682  tgellng  28524  isleag  28818  ttgelitv  28854  isspthonpth  29720  clwlkclwwlkflem  29974  clwwlkwwlksb  30024  isfxp  33127  lindflbs  33334  ply1degleel  33546  algextdeglem7  33726  ismntoplly  34028  esum2dlem  34095  ntrclselnel1  44069  ntrneicls00  44101  vonvolmbl  46678  dfdfat2  47138  ipolubdm  48997  ipoglbdm  49000  isup  49191  functhinc  49459