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

Theorem mpbirand 706
 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 536 . 2 (𝜑 → (𝜃 ↔ (𝜒𝜃)))
41, 3bitr4d 285 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  mpbiran2d  707  3anibar  1326  rmob2  3821  opbrop  5612  wemapso2lem  9002  uzin  12268  supxrre1  12713  ixxun  12744  uzsplit  12976  pfxsuffeqwrdeq  14053  ello12  14867  elo12  14878  fsumss  15076  fprodss  15296  ramval  16336  issect2  17018  lspsnel5  19763  cnprest  21901  cnprest2  21902  cnt0  21958  1stccn  22075  kgencn  22168  qtopcn  22326  fbflim  22588  isflf  22605  cnflf  22614  fclscf  22637  cnfcf  22654  elbl2ps  23003  elbl2  23004  metcn  23157  txmetcn  23162  iscvs  23739  lmclimf  23915  ovolfioo  24078  ovolficc  24079  ovoliun  24116  ismbl2  24138  mbfmulc2lem  24258  mbfmax  24260  mbfposr  24263  mbfaddlem  24271  mbfsup  24275  mbfi1fseqlem4  24329  itg2monolem1  24361  itg2cnlem1  24372  tgellng  26354  isleag  26648  ttgelitv  26684  isspthonpth  27545  clwlkclwwlkflem  27796  clwwlkwwlksb  27846  fvdifsupp  30451  lindflbs  31001  ismntoplly  31388  esum2dlem  31473  ntrclselnel1  40775  ntrneicls00  40807  vonvolmbl  43315  dfdfat2  43699
 Copyright terms: Public domain W3C validator