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  3855  opbrop  5736  fvdifsupp  8150  wemapso2lem  9505  uzin  12833  supxrre1  13290  ixxun  13322  uzsplit  13557  pfxsuffeqwrdeq  14663  ello12  15482  elo12  15493  fsumss  15691  fprodss  15914  ramval  16979  issect2  17716  ellspsn5b  20901  cnprest  23176  cnprest2  23177  cnt0  23233  1stccn  23350  kgencn  23443  qtopcn  23601  fbflim  23863  isflf  23880  cnflf  23889  fclscf  23912  cnfcf  23929  elbl2ps  24277  elbl2  24278  metcn  24431  txmetcn  24436  iscvs  25027  lmclimf  25204  ovolfioo  25368  ovolficc  25369  ovoliun  25406  ismbl2  25428  mbfmulc2lem  25548  mbfmax  25550  mbfposr  25553  mbfaddlem  25561  mbfsup  25565  mbfi1fseqlem4  25619  itg2monolem1  25651  itg2cnlem1  25662  tgellng  28480  isleag  28774  ttgelitv  28810  isspthonpth  29679  clwlkclwwlkflem  29933  clwwlkwwlksb  29983  isfxp  33125  lindflbs  33350  ply1degleel  33561  algextdeglem7  33713  ismntoplly  34015  esum2dlem  34082  ntrclselnel1  44046  ntrneicls00  44078  vonvolmbl  46659  dfdfat2  47129  ipolubdm  48975  ipoglbdm  48978  isup  49169  functhinc  49437