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  2453  r19.35  3095  ceqsralv  3501  elabd2  3649  elabg  3655  ralsng  4651  dffun8  6564  ordiso2  9529  ordtypelem7  9538  cantnf  9707  rankonidlem  9842  dfac12lem3  10160  dcomex  10461  indstr2  12943  dfgcd2  16565  lublecllem  18370  tsmsgsum  24077  tsmsres  24082  tsmsxplem1  24091  caucfil  25235  isarchiofld  33339  wl-nfimf1  37544  tendoeq2  40793  naddgeoa  43418  elmapintrab  43600  inintabd  43603  cnvcnvintabd  43624  cnvintabd  43627  relexp0eq  43725  ntrkbimka  44062  ntrk0kbimka  44063  pm10.52  44389  ichnfimlem  47477  paireqne  47525