Theorem mpbirand 720

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpbiran2d  721  3anibar  1348  rmob2  3839  opbrop  5748  fvdifsupp  8191  wemapso2lem  9549  uzin  13004  supxrre1  13463  ixxun  13495  uzsplit  13733  pfxsuffeqwrdeq  14851  ello12  15688  elo12  15699  fsumss  15896  fprodss  16120  ramval  17191  issect2  17934  ellspsn5b  21275  cnprest  23612  cnprest2  23613  cnt0  23669  1stccn  23787  kgencn  23880  qtopcn  24038  fbflim  24300  isflf  24317  cnflf  24326  fclscf  24349  cnfcf  24366  elbl2ps  24713  elbl2  24714  metcn  24867  txmetcn  24872  iscvs  25453  lmclimf  25630  ovolfioo  25793  ovolficc  25794  ovoliun  25831  ismbl2  25853  mbfmulc2lem  25973  mbfmax  25975  mbfposr  25978  mbfaddlem  25986  mbfsup  25990  mbfi1fseqlem4  26044  itg2monolem1  26076  itg2cnlem1  26087  tgellng  29021  isleag  29371  ttgelitv  29465  isspthonpth  30340  clwlkclwwlkflem  30600  clwwlkwwlksb  30650  suppgsumssiun  33679  isfxp  33775  lindflbs  33980  ply1degleel  34173  selvply1rhmlem2  34199  algextdeglem7  34401  ismntoplly  34703  esum2dlem  34770  brlexod  35938  brr0d  35940  maxssj0  35945  ntrclselnel1  45150  ntrneicls00  45182  vonvolmbl  47764  dfdfat2  48291  crngprmringidom  49531  ipolubdm  50194  ipoglbdm  50197  isup  50389  functhinc  50676