![]() |
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 353 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: mt2bi 356 pm4.83 1008 trut 1514 equsv 1961 equsalv 2197 equsal 2353 2sb6rf 2421 sb4b 2425 sbequ8 2469 ralv 3442 relop 5575 acsfn0 16801 cmpsub 21727 ballotlemodife 31433 bj-sbievw1 33700 bj-sbievw 33702 bj-ralvw 33728 wl-equsalvw 34260 wl-equsald 34261 lub0N 35810 glb0N 35814 |
Copyright terms: Public domain | W3C validator |