Theorem mpbirand 704

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

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

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 397

This theorem is referenced by:  mpbiran2d  705  3anibar  1328  rmob2  3825  opbrop  5684  wemapso2lem  9311  uzin  12618  supxrre1  13064  ixxun  13095  uzsplit  13328  pfxsuffeqwrdeq  14411  ello12  15225  elo12  15236  fsumss  15437  fprodss  15658  ramval  16709  issect2  17466  lspsnel5  20257  cnprest  22440  cnprest2  22441  cnt0  22497  1stccn  22614  kgencn  22707  qtopcn  22865  fbflim  23127  isflf  23144  cnflf  23153  fclscf  23176  cnfcf  23193  elbl2ps  23542  elbl2  23543  metcn  23699  txmetcn  23704  iscvs  24290  lmclimf  24468  ovolfioo  24631  ovolficc  24632  ovoliun  24669  ismbl2  24691  mbfmulc2lem  24811  mbfmax  24813  mbfposr  24816  mbfaddlem  24824  mbfsup  24828  mbfi1fseqlem4  24883  itg2monolem1  24915  itg2cnlem1  24926  tgellng  26914  isleag  27208  ttgelitv  27250  isspthonpth  28117  clwlkclwwlkflem  28368  clwwlkwwlksb  28418  fvdifsupp  31018  lindflbs  31574  ismntoplly  31975  esum2dlem  32060  ntrclselnel1  41667  ntrneicls00  41699  vonvolmbl  44199  dfdfat2  44620  ipolubdm  46273  ipoglbdm  46276  functhinc  46326