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  2451  r19.35  3091  ceqsralv  3478  elabd2  3621  elabgt  3623  ralsng  4627  dffun8  6514  ordiso2  9408  ordtypelem7  9417  cantnf  9590  rankonidlem  9728  dfac12lem3  10044  dcomex  10345  indstr2  12827  dfgcd2  16459  lublecllem  18266  tsmsgsum  24055  tsmsres  24060  tsmsxplem1  24069  caucfil  25211  isarchiofld  33175  wl-nfimf1  37591  tendoeq2  40893  naddgeoa  43511  elmapintrab  43693  inintabd  43696  cnvcnvintabd  43717  cnvintabd  43720  relexp0eq  43818  ntrkbimka  44155  ntrk0kbimka  44156  pm10.52  44482  ichnfimlem  47587  paireqne  47635