MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbirand Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mpbirand.2 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
2 mpbirand.1 . . 3 (𝜑𝜒)
32biantrurd 532 . 2 (𝜑 → (𝜃 ↔ (𝜒𝜃)))
41, 3bitr4d 282 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
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  3892  opbrop  5783  fvdifsupp  8196  wemapso2lem  9592  uzin  12918  supxrre1  13372  ixxun  13403  uzsplit  13636  pfxsuffeqwrdeq  14736  ello12  15552  elo12  15563  fsumss  15761  fprodss  15984  ramval  17046  issect2  17798  ellspsn5b  20993  cnprest  23297  cnprest2  23298  cnt0  23354  1stccn  23471  kgencn  23564  qtopcn  23722  fbflim  23984  isflf  24001  cnflf  24010  fclscf  24033  cnfcf  24050  elbl2ps  24399  elbl2  24400  metcn  24556  txmetcn  24561  iscvs  25160  lmclimf  25338  ovolfioo  25502  ovolficc  25503  ovoliun  25540  ismbl2  25562  mbfmulc2lem  25682  mbfmax  25684  mbfposr  25687  mbfaddlem  25695  mbfsup  25699  mbfi1fseqlem4  25753  itg2monolem1  25785  itg2cnlem1  25796  tgellng  28561  isleag  28855  ttgelitv  28897  isspthonpth  29769  clwlkclwwlkflem  30023  clwwlkwwlksb  30073  lindflbs  33407  ply1degleel  33616  algextdeglem7  33764  ismntoplly  34026  esum2dlem  34093  ntrclselnel1  44070  ntrneicls00  44102  vonvolmbl  46676  dfdfat2  47140  ipolubdm  48876  ipoglbdm  48879  isup  48937  functhinc  49097
  Copyright terms: Public domain W3C validator