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  3840  opbrop  5749  fvdifsupp  8172  wemapso2lem  9530  uzin  12982  supxrre1  13441  ixxun  13473  uzsplit  13710  pfxsuffeqwrdeq  14827  ello12  15663  elo12  15674  fsumss  15871  fprodss  16095  ramval  17166  issect2  17909  ellspsn5b  21250  cnprest  23587  cnprest2  23588  cnt0  23644  1stccn  23762  kgencn  23855  qtopcn  24013  fbflim  24275  isflf  24292  cnflf  24301  fclscf  24324  cnfcf  24341  elbl2ps  24688  elbl2  24689  metcn  24842  txmetcn  24847  iscvs  25428  lmclimf  25605  ovolfioo  25768  ovolficc  25769  ovoliun  25806  ismbl2  25828  mbfmulc2lem  25948  mbfmax  25950  mbfposr  25953  mbfaddlem  25961  mbfsup  25965  mbfi1fseqlem4  26019  itg2monolem1  26051  itg2cnlem1  26062  tgellng  28998  isleag  29348  ttgelitv  29442  isspthonpth  30317  clwlkclwwlkflem  30577  clwwlkwwlksb  30627  suppgsumssiun  33615  isfxp  33711  lindflbs  33916  ply1degleel  34109  selvply1rhmlem2  34135  algextdeglem7  34337  ismntoplly  34639  esum2dlem  34706  ntrclselnel1  45016  ntrneicls00  45048  vonvolmbl  47615  dfdfat2  48142  crngprmringidom  49382  ipolubdm  50039  ipoglbdm  50042  isup  50232  functhinc  50500