![]() |
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 2451 r19.35 3105 ceqsralv 3519 elabd2 3669 elabgtOLDOLD 3673 elabg 3676 sbceqalOLD 3857 ralsng 4679 dffun8 6595 ordiso2 9552 ordtypelem7 9561 cantnf 9730 rankonidlem 9865 dfac12lem3 10183 dcomex 10484 indstr2 12966 dfgcd2 16579 lublecllem 18417 tsmsgsum 24162 tsmsres 24167 tsmsxplem1 24176 caucfil 25330 isarchiofld 33326 wl-nfimf1 37506 tendoeq2 40756 naddgeoa 43383 elmapintrab 43565 inintabd 43568 cnvcnvintabd 43589 cnvintabd 43592 relexp0eq 43690 ntrkbimka 44027 ntrk0kbimka 44028 pm10.52 44360 ichnfimlem 47387 paireqne 47435 |
Copyright terms: Public domain | W3C validator |