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  3840  opbrop  5719  fvdifsupp  8110  wemapso2lem  9448  uzin  12782  supxrre1  13239  ixxun  13271  uzsplit  13506  pfxsuffeqwrdeq  14615  ello12  15433  elo12  15444  fsumss  15642  fprodss  15865  ramval  16930  issect2  17671  ellspsn5b  20938  cnprest  23214  cnprest2  23215  cnt0  23271  1stccn  23388  kgencn  23481  qtopcn  23639  fbflim  23901  isflf  23918  cnflf  23927  fclscf  23950  cnfcf  23967  elbl2ps  24314  elbl2  24315  metcn  24468  txmetcn  24473  iscvs  25064  lmclimf  25241  ovolfioo  25405  ovolficc  25406  ovoliun  25443  ismbl2  25465  mbfmulc2lem  25585  mbfmax  25587  mbfposr  25590  mbfaddlem  25598  mbfsup  25602  mbfi1fseqlem4  25656  itg2monolem1  25688  itg2cnlem1  25699  tgellng  28541  isleag  28835  ttgelitv  28871  isspthonpth  29738  clwlkclwwlkflem  29995  clwwlkwwlksb  30045  isfxp  33148  lindflbs  33355  ply1degleel  33567  algextdeglem7  33747  ismntoplly  34049  esum2dlem  34116  ntrclselnel1  44164  ntrneicls00  44196  vonvolmbl  46773  dfdfat2  47242  ipolubdm  49101  ipoglbdm  49104  isup  49295  functhinc  49563