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

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

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 400

This theorem is referenced by:  mpbiran2d  708  3anibar  1331  rmob2  3804  opbrop  5645  wemapso2lem  9168  uzin  12474  supxrre1  12920  ixxun  12951  uzsplit  13184  pfxsuffeqwrdeq  14263  ello12  15077  elo12  15088  fsumss  15289  fprodss  15510  ramval  16561  issect2  17259  lspsnel5  20032  cnprest  22186  cnprest2  22187  cnt0  22243  1stccn  22360  kgencn  22453  qtopcn  22611  fbflim  22873  isflf  22890  cnflf  22899  fclscf  22922  cnfcf  22939  elbl2ps  23287  elbl2  23288  metcn  23441  txmetcn  23446  iscvs  24024  lmclimf  24201  ovolfioo  24364  ovolficc  24365  ovoliun  24402  ismbl2  24424  mbfmulc2lem  24544  mbfmax  24546  mbfposr  24549  mbfaddlem  24557  mbfsup  24561  mbfi1fseqlem4  24616  itg2monolem1  24648  itg2cnlem1  24659  tgellng  26644  isleag  26938  ttgelitv  26974  isspthonpth  27836  clwlkclwwlkflem  28087  clwwlkwwlksb  28137  fvdifsupp  30738  lindflbs  31288  ismntoplly  31687  esum2dlem  31772  ntrclselnel1  41344  ntrneicls00  41376  vonvolmbl  43874  dfdfat2  44292  ipolubdm  45946  ipoglbdm  45949  functhinc  45999