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  2449  r19.35  3090  ceqsralv  3477  elabd2  3625  elabgt  3627  ralsng  4628  dffun8  6509  ordiso2  9401  ordtypelem7  9410  cantnf  9583  rankonidlem  9718  dfac12lem3  10034  dcomex  10335  indstr2  12822  dfgcd2  16454  lublecllem  18261  tsmsgsum  24052  tsmsres  24057  tsmsxplem1  24066  caucfil  25208  isarchiofld  33163  wl-nfimf1  37559  tendoeq2  40812  naddgeoa  43426  elmapintrab  43608  inintabd  43611  cnvcnvintabd  43632  cnvintabd  43635  relexp0eq  43733  ntrkbimka  44070  ntrk0kbimka  44071  pm10.52  44397  ichnfimlem  47493  paireqne  47541