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  3096  ceqsralv  3483  elabd2  3626  elabgt  3628  ralsng  4634  dffun8  6528  ordiso2  9432  ordtypelem7  9441  cantnf  9614  rankonidlem  9752  dfac12lem3  10068  dcomex  10369  indstr2  12852  dfgcd2  16485  lublecllem  18293  tsmsgsum  24095  tsmsres  24100  tsmsxplem1  24109  caucfil  25251  isarchiofld  33292  wl-nfimf1  37775  tendoeq2  41144  naddgeoa  43745  elmapintrab  43926  inintabd  43929  cnvcnvintabd  43950  cnvintabd  43953  relexp0eq  44051  ntrkbimka  44388  ntrk0kbimka  44389  pm10.52  44715  ichnfimlem  47817  paireqne  47865