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  3857  opbrop  5738  fvdifsupp  8152  wemapso2lem  9511  uzin  12839  supxrre1  13296  ixxun  13328  uzsplit  13563  pfxsuffeqwrdeq  14669  ello12  15488  elo12  15499  fsumss  15697  fprodss  15920  ramval  16985  issect2  17722  ellspsn5b  20907  cnprest  23182  cnprest2  23183  cnt0  23239  1stccn  23356  kgencn  23449  qtopcn  23607  fbflim  23869  isflf  23886  cnflf  23895  fclscf  23918  cnfcf  23935  elbl2ps  24283  elbl2  24284  metcn  24437  txmetcn  24442  iscvs  25033  lmclimf  25210  ovolfioo  25374  ovolficc  25375  ovoliun  25412  ismbl2  25434  mbfmulc2lem  25554  mbfmax  25556  mbfposr  25559  mbfaddlem  25567  mbfsup  25571  mbfi1fseqlem4  25625  itg2monolem1  25657  itg2cnlem1  25668  tgellng  28486  isleag  28780  ttgelitv  28816  isspthonpth  29685  clwlkclwwlkflem  29939  clwwlkwwlksb  29989  isfxp  33131  lindflbs  33356  ply1degleel  33567  algextdeglem7  33719  ismntoplly  34021  esum2dlem  34088  ntrclselnel1  44039  ntrneicls00  44071  vonvolmbl  46652  dfdfat2  47119  ipolubdm  48965  ipoglbdm  48968  isup  49159  functhinc  49427