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  3830  opbrop  5729  fvdifsupp  8121  wemapso2lem  9467  uzin  12824  supxrre1  13282  ixxun  13314  uzsplit  13550  pfxsuffeqwrdeq  14660  ello12  15478  elo12  15489  fsumss  15687  fprodss  15913  ramval  16979  issect2  17721  ellspsn5b  20990  cnprest  23254  cnprest2  23255  cnt0  23311  1stccn  23428  kgencn  23521  qtopcn  23679  fbflim  23941  isflf  23958  cnflf  23967  fclscf  23990  cnfcf  24007  elbl2ps  24354  elbl2  24355  metcn  24508  txmetcn  24513  iscvs  25094  lmclimf  25271  ovolfioo  25434  ovolficc  25435  ovoliun  25472  ismbl2  25494  mbfmulc2lem  25614  mbfmax  25616  mbfposr  25619  mbfaddlem  25627  mbfsup  25631  mbfi1fseqlem4  25685  itg2monolem1  25717  itg2cnlem1  25728  tgellng  28621  isleag  28915  ttgelitv  28951  isspthonpth  29817  clwlkclwwlkflem  30074  clwwlkwwlksb  30124  suppgsumssiun  33133  isfxp  33229  lindflbs  33439  ply1degleel  33655  algextdeglem7  33867  ismntoplly  34169  esum2dlem  34236  ntrclselnel1  44484  ntrneicls00  44516  vonvolmbl  47089  dfdfat2  47576  ipolubdm  49462  ipoglbdm  49465  isup  49655  functhinc  49923