| 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 360 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) | |
| 2 | 1 | bicomd 223 | 1 ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: pm5.4 388 imim21b 394 dvelimdf 2454 r19.35 3108 ceqsralv 3522 elabd2 3670 elabg 3676 sbceqalOLD 3852 ralsng 4675 dffun8 6594 ordiso2 9555 ordtypelem7 9564 cantnf 9733 rankonidlem 9868 dfac12lem3 10186 dcomex 10487 indstr2 12969 dfgcd2 16583 lublecllem 18405 tsmsgsum 24147 tsmsres 24152 tsmsxplem1 24161 caucfil 25317 isarchiofld 33347 wl-nfimf1 37527 tendoeq2 40776 naddgeoa 43407 elmapintrab 43589 inintabd 43592 cnvcnvintabd 43613 cnvintabd 43616 relexp0eq 43714 ntrkbimka 44051 ntrk0kbimka 44052 pm10.52 44384 ichnfimlem 47450 paireqne 47498 |
| Copyright terms: Public domain | W3C validator |