Theorem mpbirand 706

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

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

This theorem is referenced by:  mpbiran2d  707  3anibar  1329  rmob2  3914  opbrop  5797  fvdifsupp  8212  wemapso2lem  9621  uzin  12943  supxrre1  13392  ixxun  13423  uzsplit  13656  pfxsuffeqwrdeq  14746  ello12  15562  elo12  15573  fsumss  15773  fprodss  15996  ramval  17055  issect2  17815  ellspsn5b  21016  cnprest  23318  cnprest2  23319  cnt0  23375  1stccn  23492  kgencn  23585  qtopcn  23743  fbflim  24005  isflf  24022  cnflf  24031  fclscf  24054  cnfcf  24071  elbl2ps  24420  elbl2  24421  metcn  24577  txmetcn  24582  iscvs  25179  lmclimf  25357  ovolfioo  25521  ovolficc  25522  ovoliun  25559  ismbl2  25581  mbfmulc2lem  25701  mbfmax  25703  mbfposr  25706  mbfaddlem  25714  mbfsup  25718  mbfi1fseqlem4  25773  itg2monolem1  25805  itg2cnlem1  25816  tgellng  28579  isleag  28873  ttgelitv  28915  isspthonpth  29785  clwlkclwwlkflem  30036  clwwlkwwlksb  30086  lindflbs  33372  ply1degleel  33581  algextdeglem7  33714  ismntoplly  33971  esum2dlem  34056  ntrclselnel1  44019  ntrneicls00  44051  vonvolmbl  46582  dfdfat2  47043  ipolubdm  48659  ipoglbdm  48662  functhinc  48712