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  2448  r19.35  3089  ceqsralv  3491  elabd2  3639  elabgt  3641  ralsng  4642  dffun8  6547  ordiso2  9475  ordtypelem7  9484  cantnf  9653  rankonidlem  9788  dfac12lem3  10106  dcomex  10407  indstr2  12893  dfgcd2  16523  lublecllem  18326  tsmsgsum  24033  tsmsres  24038  tsmsxplem1  24047  caucfil  25190  isarchiofld  33302  wl-nfimf1  37521  tendoeq2  40775  naddgeoa  43390  elmapintrab  43572  inintabd  43575  cnvcnvintabd  43596  cnvintabd  43599  relexp0eq  43697  ntrkbimka  44034  ntrk0kbimka  44035  pm10.52  44361  ichnfimlem  47468  paireqne  47516