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 223	1 ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))

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  2457  nfabdwOLD  2933  r19.35  3114  ceqsralv  3531  elabd2  3683  elabgtOLDOLD  3687  elabg  3690  sbceqalOLD  3871  ralsng  4697  dffun8  6606  ordiso2  9584  ordtypelem7  9593  cantnf  9762  rankonidlem  9897  dfac12lem3  10215  dcomex  10516  indstr2  12992  dfgcd2  16593  lublecllem  18430  tsmsgsum  24168  tsmsres  24173  tsmsxplem1  24182  caucfil  25336  isarchiofld  33312  wl-nfimf1  37480  tendoeq2  40731  naddgeoa  43356  elmapintrab  43538  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  relexp0eq  43663  ntrkbimka  44000  ntrk0kbimka  44001  pm10.52  44334  ichnfimlem  47337  paireqne  47385