Theorem mpbirand 705

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpbiran2d  706  3anibar  1326  rmob2  3883  opbrop  5774  fvdifsupp  8174  wemapso2lem  9575  uzin  12892  supxrre1  13341  ixxun  13372  uzsplit  13605  pfxsuffeqwrdeq  14680  ello12  15492  elo12  15503  fsumss  15703  fprodss  15924  ramval  16976  issect2  17736  lspsnel5  20883  cnprest  23223  cnprest2  23224  cnt0  23280  1stccn  23397  kgencn  23490  qtopcn  23648  fbflim  23910  isflf  23927  cnflf  23936  fclscf  23959  cnfcf  23976  elbl2ps  24325  elbl2  24326  metcn  24482  txmetcn  24487  iscvs  25084  lmclimf  25262  ovolfioo  25426  ovolficc  25427  ovoliun  25464  ismbl2  25486  mbfmulc2lem  25606  mbfmax  25608  mbfposr  25611  mbfaddlem  25619  mbfsup  25623  mbfi1fseqlem4  25678  itg2monolem1  25710  itg2cnlem1  25721  tgellng  28413  isleag  28707  ttgelitv  28749  isspthonpth  29619  clwlkclwwlkflem  29870  clwwlkwwlksb  29920  lindflbs  33156  ply1degleel  33336  algextdeglem7  33461  ismntoplly  33696  esum2dlem  33781  ntrclselnel1  43552  ntrneicls00  43584  vonvolmbl  46112  dfdfat2  46571  ipolubdm  48110  ipoglbdm  48113  functhinc  48163