Theorem mpbirand 707

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  708  3anibar  1328  rmob2  3901  opbrop  5786  fvdifsupp  8195  wemapso2lem  9590  uzin  12916  supxrre1  13369  ixxun  13400  uzsplit  13633  pfxsuffeqwrdeq  14733  ello12  15549  elo12  15560  fsumss  15758  fprodss  15981  ramval  17042  issect2  17802  ellspsn5b  21011  cnprest  23313  cnprest2  23314  cnt0  23370  1stccn  23487  kgencn  23580  qtopcn  23738  fbflim  24000  isflf  24017  cnflf  24026  fclscf  24049  cnfcf  24066  elbl2ps  24415  elbl2  24416  metcn  24572  txmetcn  24577  iscvs  25174  lmclimf  25352  ovolfioo  25516  ovolficc  25517  ovoliun  25554  ismbl2  25576  mbfmulc2lem  25696  mbfmax  25698  mbfposr  25701  mbfaddlem  25709  mbfsup  25713  mbfi1fseqlem4  25768  itg2monolem1  25800  itg2cnlem1  25811  tgellng  28576  isleag  28870  ttgelitv  28912  isspthonpth  29782  clwlkclwwlkflem  30033  clwwlkwwlksb  30083  lindflbs  33387  ply1degleel  33596  algextdeglem7  33729  ismntoplly  33988  esum2dlem  34073  ntrclselnel1  44047  ntrneicls00  44079  vonvolmbl  46617  dfdfat2  47078  ipolubdm  48776  ipoglbdm  48779  functhinc  48845