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  2454  r19.35  3108  ceqsralv  3522  elabd2  3670  elabg  3676  sbceqalOLD  3852  ralsng  4675  dffun8  6594  ordiso2  9555  ordtypelem7  9564  cantnf  9733  rankonidlem  9868  dfac12lem3  10186  dcomex  10487  indstr2  12969  dfgcd2  16583  lublecllem  18405  tsmsgsum  24147  tsmsres  24152  tsmsxplem1  24161  caucfil  25317  isarchiofld  33347  wl-nfimf1  37527  tendoeq2  40776  naddgeoa  43407  elmapintrab  43589  inintabd  43592  cnvcnvintabd  43613  cnvintabd  43616  relexp0eq  43714  ntrkbimka  44051  ntrk0kbimka  44052  pm10.52  44384  ichnfimlem  47450  paireqne  47498