![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > a1bi | Structured version Visualization version GIF version |
Description: Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
Ref | Expression |
---|---|
a1bi.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
a1bi | ⊢ (𝜓 ↔ (𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a1bi.1 | . 2 ⊢ 𝜑 | |
2 | biimt 359 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) | |
3 | 1, 2 | ax-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 |