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  3844  opbrop  5730  fvdifsupp  8123  wemapso2lem  9469  uzin  12799  supxrre1  13257  ixxun  13289  uzsplit  13524  pfxsuffeqwrdeq  14633  ello12  15451  elo12  15462  fsumss  15660  fprodss  15883  ramval  16948  issect2  17690  ellspsn5b  20958  cnprest  23245  cnprest2  23246  cnt0  23302  1stccn  23419  kgencn  23512  qtopcn  23670  fbflim  23932  isflf  23949  cnflf  23958  fclscf  23981  cnfcf  23998  elbl2ps  24345  elbl2  24346  metcn  24499  txmetcn  24504  iscvs  25095  lmclimf  25272  ovolfioo  25436  ovolficc  25437  ovoliun  25474  ismbl2  25496  mbfmulc2lem  25616  mbfmax  25618  mbfposr  25621  mbfaddlem  25629  mbfsup  25633  mbfi1fseqlem4  25687  itg2monolem1  25719  itg2cnlem1  25730  tgellng  28637  isleag  28931  ttgelitv  28967  isspthonpth  29834  clwlkclwwlkflem  30091  clwwlkwwlksb  30141  suppgsumssiun  33165  isfxp  33261  lindflbs  33471  ply1degleel  33687  algextdeglem7  33900  ismntoplly  34202  esum2dlem  34269  ntrclselnel1  44402  ntrneicls00  44434  vonvolmbl  47008  dfdfat2  47477  ipolubdm  49335  ipoglbdm  49338  isup  49528  functhinc  49796