Theorem mpbirand 713

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

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

This theorem is referenced by:  mpbiran2d  714  3anibar  1336  rmob2  3831  opbrop  5723  fvdifsupp  8118  wemapso2lem  9464  uzin  12822  supxrre1  13280  ixxun  13312  uzsplit  13548  pfxsuffeqwrdeq  14658  ello12  15476  elo12  15487  fsumss  15685  fprodss  15911  ramval  16977  issect2  17719  ellspsn5b  20992  cnprest  23279  cnprest2  23280  cnt0  23336  1stccn  23453  kgencn  23546  qtopcn  23704  fbflim  23966  isflf  23983  cnflf  23992  fclscf  24015  cnfcf  24032  elbl2ps  24379  elbl2  24380  metcn  24533  txmetcn  24538  iscvs  25119  lmclimf  25296  ovolfioo  25459  ovolficc  25460  ovoliun  25497  ismbl2  25519  mbfmulc2lem  25639  mbfmax  25641  mbfposr  25644  mbfaddlem  25652  mbfsup  25656  mbfi1fseqlem4  25710  itg2monolem1  25742  itg2cnlem1  25753  tgellng  28646  isleag  28940  ttgelitv  28976  isspthonpth  29842  clwlkclwwlkflem  30099  clwwlkwwlksb  30149  suppgsumssiun  33160  isfxp  33256  lindflbs  33469  ply1degleel  33685  selvply1rhmlem2  33712  algextdeglem7  33914  ismntoplly  34216  esum2dlem  34283  ntrclselnel1  44508  ntrneicls00  44540  vonvolmbl  47111  dfdfat2  47598  ipolubdm  49484  ipoglbdm  49487  isup  49677  functhinc  49945