Theorem mpbirand 719

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpbiran2d  720  3anibar  1346  rmob2  3848  opbrop  5750  fvdifsupp  8155  wemapso2lem  9502  uzin  12889  supxrre1  13347  ixxun  13379  uzsplit  13615  pfxsuffeqwrdeq  14725  ello12  15557  elo12  15568  fsumss  15766  fprodss  15992  ramval  17058  issect2  17801  ellspsn5b  21085  cnprest  23407  cnprest2  23408  cnt0  23464  1stccn  23581  kgencn  23674  qtopcn  23832  fbflim  24094  isflf  24111  cnflf  24120  fclscf  24143  cnfcf  24160  elbl2ps  24507  elbl2  24508  metcn  24661  txmetcn  24666  iscvs  25247  lmclimf  25424  ovolfioo  25587  ovolficc  25588  ovoliun  25625  ismbl2  25647  mbfmulc2lem  25767  mbfmax  25769  mbfposr  25772  mbfaddlem  25780  mbfsup  25784  mbfi1fseqlem4  25838  itg2monolem1  25870  itg2cnlem1  25881  tgellng  28780  isleag  29099  ttgelitv  29141  isspthonpth  30007  clwlkclwwlkflem  30264  clwwlkwwlksb  30314  suppgsumssiun  33305  isfxp  33401  lindflbs  33608  ply1degleel  33802  selvply1rhmlem2  33828  algextdeglem7  34030  ismntoplly  34332  esum2dlem  34399  ntrclselnel1  44645  ntrneicls00  44677  vonvolmbl  47233  dfdfat2  47720  crngprmringidom  48961  ipolubdm  49616  ipoglbdm  49619  isup  49809  functhinc  50077