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 349 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) | |
2 | 1 | bicomd 212 | 1 ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: imim21b 381 dvelimdf 2323 2sb6rf 2440 elabgt 3316 sbceqal 3454 dffun8 5831 ordiso2 8303 ordtypelem7 8312 cantnf 8473 rankonidlem 8574 dfac12lem3 8850 dcomex 9152 indstr2 11643 dfgcd2 15101 lublecllem 16811 tsmsgsum 21752 tsmsres 21757 tsmsxplem1 21766 caucfil 22889 isarchiofld 29148 wl-nfimf1 32492 tendoeq2 35080 elmapintrab 36901 inintabd 36904 cnvcnvintabd 36925 cnvintabd 36928 relexp0eq 37012 ntrkbimka 37356 ntrk0kbimka 37357 pm10.52 37586 |
Copyright terms: Public domain | W3C validator |