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  3844  opbrop  5754  fvdifsupp  8216  wemapso2lem  9573  uzin  13028  supxrre1  13487  ixxun  13519  uzsplit  13757  pfxsuffeqwrdeq  14875  ello12  15712  elo12  15723  fsumss  15920  fprodss  16144  ramval  17215  issect2  17958  ellspsn5b  21300  cnprest  23637  cnprest2  23638  cnt0  23694  1stccn  23812  kgencn  23905  qtopcn  24063  fbflim  24325  isflf  24342  cnflf  24351  fclscf  24374  cnfcf  24391  elbl2ps  24738  elbl2  24739  metcn  24892  txmetcn  24897  iscvs  25478  lmclimf  25655  ovolfioo  25818  ovolficc  25819  ovoliun  25856  ismbl2  25878  mbfmulc2lem  25998  mbfmax  26000  mbfposr  26003  mbfaddlem  26011  mbfsup  26015  mbfi1fseqlem4  26069  itg2monolem1  26101  itg2cnlem1  26112  tgellng  29046  isleag  29396  ttgelitv  29490  isspthonpth  30365  clwlkclwwlkflem  30625  clwwlkwwlksb  30675  suppgsumssiun  33703  isfxp  33799  lindflbs  34004  ply1degleel  34197  selvply1rhmlem2  34223  algextdeglem7  34425  ismntoplly  34727  esum2dlem  34794  brlexod  35999  brr0d  36001  maxssj0  36006  ntrclselnel1  45249  ntrneicls00  45281  vonvolmbl  47876  dfdfat2  48403  crngprmringidom  49643  ipolubdm  50306  ipoglbdm  50309  isup  50501  functhinc  50788