Theorem mpbirand 705

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 533	. 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
4	1, 3	bitr4d 281	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  mpbiran2d  706  3anibar  1329  rmob2  3885  opbrop  5771  wemapso2lem  9543  uzin  12858  supxrre1  13305  ixxun  13336  uzsplit  13569  pfxsuffeqwrdeq  14644  ello12  15456  elo12  15467  fsumss  15667  fprodss  15888  ramval  16937  issect2  17697  lspsnel5  20598  cnprest  22784  cnprest2  22785  cnt0  22841  1stccn  22958  kgencn  23051  qtopcn  23209  fbflim  23471  isflf  23488  cnflf  23497  fclscf  23520  cnfcf  23537  elbl2ps  23886  elbl2  23887  metcn  24043  txmetcn  24048  iscvs  24634  lmclimf  24812  ovolfioo  24975  ovolficc  24976  ovoliun  25013  ismbl2  25035  mbfmulc2lem  25155  mbfmax  25157  mbfposr  25160  mbfaddlem  25168  mbfsup  25172  mbfi1fseqlem4  25227  itg2monolem1  25259  itg2cnlem1  25270  tgellng  27793  isleag  28087  ttgelitv  28129  isspthonpth  28995  clwlkclwwlkflem  29246  clwwlkwwlksb  29296  fvdifsupp  31894  lindflbs  32483  ismntoplly  32993  esum2dlem  33078  ntrclselnel1  42793  ntrneicls00  42825  vonvolmbl  45363  dfdfat2  45822  ipolubdm  47565  ipoglbdm  47568  functhinc  47618