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  2453  r19.35  3095  ceqsralv  3470  elabd2  3612  elabgt  3614  ralsng  4619  dffun8  6526  ordiso2  9430  ordtypelem7  9439  cantnf  9614  rankonidlem  9752  dfac12lem3  10068  dcomex  10369  indstr2  12877  dfgcd2  16515  lublecllem  18324  tsmsgsum  24104  tsmsres  24109  tsmsxplem1  24118  caucfil  25250  isarchiofld  33260  mh-regprimbi  36727  wl-nfimf1  37851  tendoeq2  41220  naddgeoa  43822  elmapintrab  44003  inintabd  44006  cnvcnvintabd  44027  cnvintabd  44030  relexp0eq  44128  ntrkbimka  44465  ntrk0kbimka  44466  pm10.52  44792  ichnfimlem  47923  paireqne  47971