| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pm5.5 | Structured version Visualization version GIF version | ||
| Description: Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
| Ref | Expression |
|---|---|
| pm5.5 | ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biimt 363 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) | |
| 2 | 1 | bicomd 226 | 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: pm5.4 392 imbibi 395 imim21b 399 dvelimdf 2483 r19.35 3123 ceqsralv 3497 elabd2 3632 elabgt 3634 ralsng 4637 dffun8 6553 ordiso2 9465 ordtypelem7 9474 cantnf 9650 rankonidlem 9788 dfac12lem3 10117 dcomex 10419 indstr2 12939 dfgcd2 16592 lublecllem 18402 tsmsgsum 24253 tsmsres 24258 tsmsxplem1 24267 caucfil 25399 isarchiofld 33427 mh-regprimbi 36913 wl-nfimf1 38036 tendoeq2 41405 naddgeoa 43978 elmapintrab 44159 inintabd 44162 cnvcnvintabd 44183 cnvintabd 44186 relexp0eq 44284 ntrkbimka 44621 ntrk0kbimka 44622 pm10.52 44934 ichnfimlem 48068 paireqne 48116 |
| Copyright terms: Public domain | W3C validator |