Theorem pm5.5 361

Description: Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm5.5	⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))

Proof of Theorem pm5.5

Step	Hyp	Ref	Expression
1		biimt 360	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
2	1	bicomd 222	1 ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))

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  394  dvelimdf  2449  nfabdwOLD  2930  ceqsalv  3457  ceqsralv  3459  elabd2  3594  elabgtOLD  3597  elabg  3600  sbceqalOLD  3779  ralsng  4606  dffun8  6446  ordiso2  9204  ordtypelem7  9213  cantnf  9381  rankonidlem  9517  dfac12lem3  9832  dcomex  10134  indstr2  12596  dfgcd2  16182  lublecllem  17993  tsmsgsum  23198  tsmsres  23203  tsmsxplem1  23212  caucfil  24352  isarchiofld  31418  wl-nfimf1  35612  tendoeq2  38715  elmapintrab  41073  inintabd  41076  cnvcnvintabd  41097  cnvintabd  41100  relexp0eq  41198  ntrkbimka  41537  ntrk0kbimka  41538  pm10.52  41872  ichnfimlem  44803  paireqne  44851