Theorem mpbirand 708

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  709  3anibar  1331  rmob2  3843  opbrop  5723  fvdifsupp  8115  wemapso2lem  9461  uzin  12791  supxrre1  13249  ixxun  13281  uzsplit  13516  pfxsuffeqwrdeq  14625  ello12  15443  elo12  15454  fsumss  15652  fprodss  15875  ramval  16940  issect2  17682  ellspsn5b  20950  cnprest  23237  cnprest2  23238  cnt0  23294  1stccn  23411  kgencn  23504  qtopcn  23662  fbflim  23924  isflf  23941  cnflf  23950  fclscf  23973  cnfcf  23990  elbl2ps  24337  elbl2  24338  metcn  24491  txmetcn  24496  iscvs  25087  lmclimf  25264  ovolfioo  25428  ovolficc  25429  ovoliun  25466  ismbl2  25488  mbfmulc2lem  25608  mbfmax  25610  mbfposr  25613  mbfaddlem  25621  mbfsup  25625  mbfi1fseqlem4  25679  itg2monolem1  25711  itg2cnlem1  25722  tgellng  28608  isleag  28902  ttgelitv  28938  isspthonpth  29805  clwlkclwwlkflem  30062  clwwlkwwlksb  30112  isfxp  33231  lindflbs  33441  ply1degleel  33657  algextdeglem7  33861  ismntoplly  34163  esum2dlem  34230  ntrclselnel1  44334  ntrneicls00  44366  vonvolmbl  46941  dfdfat2  47410  ipolubdm  49268  ipoglbdm  49271  isup  49461  functhinc  49729