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 364 | . 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 393 imim21b 398 dvelimdf 2448 nfabdwOLD 2928 ceqsalv 3443 ceqsralv 3445 elabd2 3579 elabgtOLD 3582 elabg 3585 sbceqalOLD 3762 ralsng 4589 dffun8 6408 ordiso2 9131 ordtypelem7 9140 cantnf 9308 rankonidlem 9444 dfac12lem3 9759 dcomex 10061 indstr2 12523 dfgcd2 16106 lublecllem 17866 tsmsgsum 23036 tsmsres 23041 tsmsxplem1 23050 caucfil 24180 isarchiofld 31235 wl-nfimf1 35422 tendoeq2 38525 elmapintrab 40860 inintabd 40863 cnvcnvintabd 40884 cnvintabd 40887 relexp0eq 40986 ntrkbimka 41325 ntrk0kbimka 41326 pm10.52 41656 ichnfimlem 44588 paireqne 44636 |
Copyright terms: Public domain | W3C validator |