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  2447  r19.35  3087  ceqsralv  3479  elabd2  3627  elabgt  3629  ralsng  4629  dffun8  6514  ordiso2  9426  ordtypelem7  9435  cantnf  9608  rankonidlem  9743  dfac12lem3  10059  dcomex  10360  indstr2  12846  dfgcd2  16475  lublecllem  18282  tsmsgsum  24042  tsmsres  24047  tsmsxplem1  24056  caucfil  25199  isarchiofld  33151  wl-nfimf1  37499  tendoeq2  40753  naddgeoa  43367  elmapintrab  43549  inintabd  43552  cnvcnvintabd  43573  cnvintabd  43576  relexp0eq  43674  ntrkbimka  44011  ntrk0kbimka  44012  pm10.52  44338  ichnfimlem  47448  paireqne  47496