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

Theorem mpbiran2 992
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
Hypotheses
Ref Expression
mpbiran2.1 𝜒
mpbiran2.2 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
mpbiran2 (𝜑𝜓)

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2 (𝜑 ↔ (𝜓𝜒))
2 mpbiran2.1 . . 3 𝜒
32biantru 527 . 2 (𝜓 ↔ (𝜓𝜒))
41, 3bitr4i 267 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  pm5.62  996  reueq  3537  ss0b  4108  eusv1  5001  eusv2nf  5005  eusv2  5006  opthprc  5316  sosn  5337  opelresOLD  5553  fdmrn  6217  f1cnvcnv  6262  fores  6277  f1orn  6300  funfv  6419  dfoprab2  6858  elxp7  7360  tpostpos  7533  canthwe  9657  recmulnq  9970  opelreal  10135  elreal2  10137  eqresr  10142  elnn1uz2  11950  faclbnd4lem1  13266  isprm2  15589  joindm  17196  meetdm  17210  symgbas0  18006  efgs1  18340  toptopon  20916  ist1-3  21347  perfcls  21363  prdsxmetlem  22366  rusgrprc  26688  hhsssh2  28428  choc0  28486  chocnul  28488  shlesb1i  28546  adjeu  29049  isarchi  30037  derang0  31450  brtxp  32285  brpprod  32290  dfon3  32297  brtxpsd  32299  topmeet  32657  filnetlem2  32672  filnetlem3  32673  bj-rabtrALT  33225  bj-snsetex  33249  relowlpssretop  33515  poimirlem28  33742  fdc  33846  0totbnd  33877  heiborlem3  33917  cossssid  34532  cnvrefrelcoss2  34598  ifpid3g  38331  elintima  38439
  Copyright terms: Public domain W3C validator