Theorem mpbirand 703

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 281	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  mpbiran2d  704  3anibar  1327  rmob2  3821  opbrop  5674  wemapso2lem  9241  uzin  12547  supxrre1  12993  ixxun  13024  uzsplit  13257  pfxsuffeqwrdeq  14339  ello12  15153  elo12  15164  fsumss  15365  fprodss  15586  ramval  16637  issect2  17383  lspsnel5  20172  cnprest  22348  cnprest2  22349  cnt0  22405  1stccn  22522  kgencn  22615  qtopcn  22773  fbflim  23035  isflf  23052  cnflf  23061  fclscf  23084  cnfcf  23101  elbl2ps  23450  elbl2  23451  metcn  23605  txmetcn  23610  iscvs  24196  lmclimf  24373  ovolfioo  24536  ovolficc  24537  ovoliun  24574  ismbl2  24596  mbfmulc2lem  24716  mbfmax  24718  mbfposr  24721  mbfaddlem  24729  mbfsup  24733  mbfi1fseqlem4  24788  itg2monolem1  24820  itg2cnlem1  24831  tgellng  26818  isleag  27112  ttgelitv  27153  isspthonpth  28018  clwlkclwwlkflem  28269  clwwlkwwlksb  28319  fvdifsupp  30920  lindflbs  31476  ismntoplly  31875  esum2dlem  31960  ntrclselnel1  41556  ntrneicls00  41588  vonvolmbl  44089  dfdfat2  44507  ipolubdm  46161  ipoglbdm  46164  functhinc  46214