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

Theorem a1bi 361
Description: Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Hypothesis
Ref Expression
a1bi.1 𝜑
Assertion
Ref Expression
a1bi (𝜓 ↔ (𝜑𝜓))

Proof of Theorem a1bi
StepHypRef Expression
1 a1bi.1 . 2 𝜑
2 biimt 359 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  mt2bi  362  pm4.83  1022  trut  1539  equsv  1998  equsalv  2253  equsal  2411  2sb6rf  2467  sb4b  2469  sbequ8  2495  ralv  3498  ceqsal  3509  ceqsalv  3511  sbceqal  3844  relop  5857  acsfn0  17647  cmpsub  23324  ballotlemodife  34150  bj-equsvt  36289  bj-sbievw1  36355  bj-sbievw  36357  bj-ralvw  36390  wl-2mintru2  37003  wl-equsalvw  37038  wl-equsald  37039  wl-equsaldv  37040  lub0N  38693  glb0N  38697
  Copyright terms: Public domain W3C validator