Theorem mpbirand 719

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

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

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 401

This theorem is referenced by:  mpbiran2d  720  3anibar  1348  rmob2  3847  opbrop  5761  fvdifsupp  8168  wemapso2lem  9515  uzin  12899  supxrre1  13357  ixxun  13389  uzsplit  13626  pfxsuffeqwrdeq  14737  ello12  15569  elo12  15580  fsumss  15778  fprodss  16004  ramval  17069  issect2  17812  ellspsn5b  21097  cnprest  23427  cnprest2  23428  cnt0  23484  1stccn  23601  kgencn  23694  qtopcn  23852  fbflim  24114  isflf  24131  cnflf  24140  fclscf  24163  cnfcf  24180  elbl2ps  24527  elbl2  24528  metcn  24681  txmetcn  24686  iscvs  25267  lmclimf  25444  ovolfioo  25607  ovolficc  25608  ovoliun  25645  ismbl2  25667  mbfmulc2lem  25787  mbfmax  25789  mbfposr  25792  mbfaddlem  25800  mbfsup  25804  mbfi1fseqlem4  25858  itg2monolem1  25890  itg2cnlem1  25901  tgellng  28800  isleag  29142  ttgelitv  29210  isspthonpth  30076  clwlkclwwlkflem  30333  clwwlkwwlksb  30383  suppgsumssiun  33370  isfxp  33466  lindflbs  33670  ply1degleel  33863  selvply1rhmlem2  33889  algextdeglem7  34091  ismntoplly  34393  esum2dlem  34460  ntrclselnel1  44763  ntrneicls00  44795  vonvolmbl  47355  dfdfat2  47842  crngprmringidom  49083  ipolubdm  49742  ipoglbdm  49745  isup  49935  functhinc  50203