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  3843  opbrop  5757  fvdifsupp  8173  wemapso2lem  9528  uzin  12927  supxrre1  13386  ixxun  13418  uzsplit  13655  pfxsuffeqwrdeq  14771  ello12  15607  elo12  15618  fsumss  15815  fprodss  16041  ramval  17106  issect2  17849  ellspsn5b  21185  cnprest  23520  cnprest2  23521  cnt0  23577  1stccn  23695  kgencn  23788  qtopcn  23946  fbflim  24208  isflf  24225  cnflf  24234  fclscf  24257  cnfcf  24274  elbl2ps  24621  elbl2  24622  metcn  24775  txmetcn  24780  iscvs  25361  lmclimf  25538  ovolfioo  25701  ovolficc  25702  ovoliun  25739  ismbl2  25761  mbfmulc2lem  25881  mbfmax  25883  mbfposr  25886  mbfaddlem  25894  mbfsup  25898  mbfi1fseqlem4  25952  itg2monolem1  25984  itg2cnlem1  25995  tgellng  28903  isleag  29253  ttgelitv  29347  isspthonpth  30222  clwlkclwwlkflem  30482  clwwlkwwlksb  30532  suppgsumssiun  33520  isfxp  33616  lindflbs  33820  ply1degleel  34013  selvply1rhmlem2  34039  algextdeglem7  34241  ismntoplly  34543  esum2dlem  34610  ntrclselnel1  44905  ntrneicls00  44937  vonvolmbl  47497  dfdfat2  48024  crngprmringidom  49264  ipolubdm  49921  ipoglbdm  49924  isup  50114  functhinc  50382