Theorem mpbirand 706

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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  mpbiran2d  707  3anibar  1327  rmob2  3882  opbrop  5769  wemapso2lem  9567  uzin  12884  supxrre1  13333  ixxun  13364  uzsplit  13597  pfxsuffeqwrdeq  14672  ello12  15484  elo12  15495  fsumss  15695  fprodss  15916  ramval  16968  issect2  17728  lspsnel5  20868  cnprest  23180  cnprest2  23181  cnt0  23237  1stccn  23354  kgencn  23447  qtopcn  23605  fbflim  23867  isflf  23884  cnflf  23893  fclscf  23916  cnfcf  23933  elbl2ps  24282  elbl2  24283  metcn  24439  txmetcn  24444  iscvs  25041  lmclimf  25219  ovolfioo  25383  ovolficc  25384  ovoliun  25421  ismbl2  25443  mbfmulc2lem  25563  mbfmax  25565  mbfposr  25568  mbfaddlem  25576  mbfsup  25580  mbfi1fseqlem4  25635  itg2monolem1  25667  itg2cnlem1  25678  tgellng  28344  isleag  28638  ttgelitv  28680  isspthonpth  29550  clwlkclwwlkflem  29801  clwwlkwwlksb  29851  fvdifsupp  32449  lindflbs  33034  ply1degleel  33198  algextdeglem7  33327  ismntoplly  33562  esum2dlem  33647  ntrclselnel1  43410  ntrneicls00  43442  vonvolmbl  45972  dfdfat2  46431  ipolubdm  47921  ipoglbdm  47924  functhinc  47974