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

Theorem a1bi 366
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 364 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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
This theorem is referenced by:  mt2bi  367  pm4.83  1022  trut  1544  equsv  2009  equsalv  2265  equsal  2428  2sb6rf  2486  sb4b  2488  sb4bOLD  2489  sbequ8  2520  ralv  3466  relop  5685  acsfn0  16923  cmpsub  22005  ballotlemodife  31865  bj-sbievw1  34281  bj-sbievw  34283  bj-ralvw  34316  wl-2mintru2  34905  wl-equsalvw  34940  wl-equsald  34941  lub0N  36482  glb0N  36486
  Copyright terms: Public domain W3C validator