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  3892  opbrop  5783  fvdifsupp  8196  wemapso2lem  9592  uzin  12918  supxrre1  13372  ixxun  13403  uzsplit  13636  pfxsuffeqwrdeq  14736  ello12  15552  elo12  15563  fsumss  15761  fprodss  15984  ramval  17046  issect2  17798  ellspsn5b  20993  cnprest  23297  cnprest2  23298  cnt0  23354  1stccn  23471  kgencn  23564  qtopcn  23722  fbflim  23984  isflf  24001  cnflf  24010  fclscf  24033  cnfcf  24050  elbl2ps  24399  elbl2  24400  metcn  24556  txmetcn  24561  iscvs  25160  lmclimf  25338  ovolfioo  25502  ovolficc  25503  ovoliun  25540  ismbl2  25562  mbfmulc2lem  25682  mbfmax  25684  mbfposr  25687  mbfaddlem  25695  mbfsup  25699  mbfi1fseqlem4  25753  itg2monolem1  25785  itg2cnlem1  25796  tgellng  28561  isleag  28855  ttgelitv  28897  isspthonpth  29769  clwlkclwwlkflem  30023  clwwlkwwlksb  30073  lindflbs  33407  ply1degleel  33616  algextdeglem7  33764  ismntoplly  34026  esum2dlem  34093  ntrclselnel1  44070  ntrneicls00  44102  vonvolmbl  46676  dfdfat2  47140  ipolubdm  48876  ipoglbdm  48879  isup  48937  functhinc  49097