Theorem mpbirand 707

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  708  3anibar  1330  rmob2  3846  opbrop  5721  fvdifsupp  8111  wemapso2lem  9463  uzin  12793  supxrre1  13250  ixxun  13282  uzsplit  13517  pfxsuffeqwrdeq  14622  ello12  15441  elo12  15452  fsumss  15650  fprodss  15873  ramval  16938  issect2  17679  ellspsn5b  20916  cnprest  23192  cnprest2  23193  cnt0  23249  1stccn  23366  kgencn  23459  qtopcn  23617  fbflim  23879  isflf  23896  cnflf  23905  fclscf  23928  cnfcf  23945  elbl2ps  24293  elbl2  24294  metcn  24447  txmetcn  24452  iscvs  25043  lmclimf  25220  ovolfioo  25384  ovolficc  25385  ovoliun  25422  ismbl2  25444  mbfmulc2lem  25564  mbfmax  25566  mbfposr  25569  mbfaddlem  25577  mbfsup  25581  mbfi1fseqlem4  25635  itg2monolem1  25667  itg2cnlem1  25678  tgellng  28516  isleag  28810  ttgelitv  28846  isspthonpth  29712  clwlkclwwlkflem  29966  clwwlkwwlksb  30016  isfxp  33123  lindflbs  33326  ply1degleel  33537  algextdeglem7  33689  ismntoplly  33991  esum2dlem  34058  ntrclselnel1  44030  ntrneicls00  44062  vonvolmbl  46643  dfdfat2  47113  ipolubdm  48959  ipoglbdm  48962  isup  49153  functhinc  49421