Theorem mpbirand 703

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpbiran2d  704  3anibar  1327  rmob2  3885  opbrop  5772  wemapso2lem  9549  uzin  12866  supxrre1  13313  ixxun  13344  uzsplit  13577  pfxsuffeqwrdeq  14652  ello12  15464  elo12  15475  fsumss  15675  fprodss  15896  ramval  16945  issect2  17705  lspsnel5  20750  cnprest  23013  cnprest2  23014  cnt0  23070  1stccn  23187  kgencn  23280  qtopcn  23438  fbflim  23700  isflf  23717  cnflf  23726  fclscf  23749  cnfcf  23766  elbl2ps  24115  elbl2  24116  metcn  24272  txmetcn  24277  iscvs  24874  lmclimf  25052  ovolfioo  25216  ovolficc  25217  ovoliun  25254  ismbl2  25276  mbfmulc2lem  25396  mbfmax  25398  mbfposr  25401  mbfaddlem  25409  mbfsup  25413  mbfi1fseqlem4  25468  itg2monolem1  25500  itg2cnlem1  25511  tgellng  28071  isleag  28365  ttgelitv  28407  isspthonpth  29273  clwlkclwwlkflem  29524  clwwlkwwlksb  29574  fvdifsupp  32174  lindflbs  32769  ply1degleel  32941  algextdeglem7  33068  ismntoplly  33303  esum2dlem  33388  ntrclselnel1  43110  ntrneicls00  43142  vonvolmbl  45675  dfdfat2  46134  ipolubdm  47699  ipoglbdm  47702  functhinc  47752