Theorem mpbirand 708

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  709  3anibar  1331  rmob2  3831  opbrop  5720  fvdifsupp  8112  wemapso2lem  9458  uzin  12813  supxrre1  13271  ixxun  13303  uzsplit  13539  pfxsuffeqwrdeq  14649  ello12  15467  elo12  15478  fsumss  15676  fprodss  15902  ramval  16968  issect2  17710  ellspsn5b  20979  cnprest  23263  cnprest2  23264  cnt0  23320  1stccn  23437  kgencn  23530  qtopcn  23688  fbflim  23950  isflf  23967  cnflf  23976  fclscf  23999  cnfcf  24016  elbl2ps  24363  elbl2  24364  metcn  24517  txmetcn  24522  iscvs  25103  lmclimf  25280  ovolfioo  25443  ovolficc  25444  ovoliun  25481  ismbl2  25503  mbfmulc2lem  25623  mbfmax  25625  mbfposr  25628  mbfaddlem  25636  mbfsup  25640  mbfi1fseqlem4  25694  itg2monolem1  25726  itg2cnlem1  25737  tgellng  28640  isleag  28934  ttgelitv  28970  isspthonpth  29837  clwlkclwwlkflem  30094  clwwlkwwlksb  30144  suppgsumssiun  33153  isfxp  33249  lindflbs  33459  ply1degleel  33675  algextdeglem7  33888  ismntoplly  34190  esum2dlem  34257  ntrclselnel1  44499  ntrneicls00  44531  vonvolmbl  47104  dfdfat2  47573  ipolubdm  49459  ipoglbdm  49462  isup  49652  functhinc  49920