![]() |
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 222 | 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: pm5.4 389 imim21b 395 dvelimdf 2447 nfabdwOLD 2926 r19.35 3107 ceqsralv 3511 elabd2 3656 elabgtOLD 3659 elabg 3662 sbceqalOLD 3840 ralsng 4670 dffun8 6565 ordiso2 9492 ordtypelem7 9501 cantnf 9670 rankonidlem 9805 dfac12lem3 10122 dcomex 10424 indstr2 12893 dfgcd2 16470 lublecllem 18295 tsmsgsum 23572 tsmsres 23577 tsmsxplem1 23586 caucfil 24729 isarchiofld 32297 wl-nfimf1 36197 tendoeq2 39448 naddgeoa 41914 elmapintrab 42096 inintabd 42099 cnvcnvintabd 42120 cnvintabd 42123 relexp0eq 42221 ntrkbimka 42558 ntrk0kbimka 42559 pm10.52 42893 ichnfimlem 45901 paireqne 45949 |
Copyright terms: Public domain | W3C validator |