Theorem mpbirand 717

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpbiran2d  718  3anibar  1342  rmob2  3845  opbrop  5743  fvdifsupp  8146  wemapso2lem  9497  uzin  12872  supxrre1  13330  ixxun  13362  uzsplit  13598  pfxsuffeqwrdeq  14708  ello12  15526  elo12  15537  fsumss  15735  fprodss  15961  ramval  17027  issect2  17770  ellspsn5b  21042  cnprest  23329  cnprest2  23330  cnt0  23386  1stccn  23503  kgencn  23596  qtopcn  23754  fbflim  24016  isflf  24033  cnflf  24042  fclscf  24065  cnfcf  24082  elbl2ps  24429  elbl2  24430  metcn  24583  txmetcn  24588  iscvs  25169  lmclimf  25346  ovolfioo  25509  ovolficc  25510  ovoliun  25547  ismbl2  25569  mbfmulc2lem  25689  mbfmax  25691  mbfposr  25694  mbfaddlem  25702  mbfsup  25706  mbfi1fseqlem4  25760  itg2monolem1  25792  itg2cnlem1  25803  tgellng  28699  isleag  28993  ttgelitv  29029  isspthonpth  29895  clwlkclwwlkflem  30152  clwwlkwwlksb  30202  suppgsumssiun  33213  isfxp  33309  lindflbs  33526  ply1degleel  33752  selvply1rhmlem2  33779  algextdeglem7  33981  ismntoplly  34283  esum2dlem  34350  ntrclselnel1  44597  ntrneicls00  44629  vonvolmbl  47199  dfdfat2  47686  ipolubdm  49572  ipoglbdm  49575  isup  49765  functhinc  50033