Theorem pm5.5 362

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 361	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
2	1	bicomd 224	1 ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  pm5.4  389  imim21b  395  dvelimdf  2457  r19.35  3098  ceqsralv  3473  elabd2  3615  elabgt  3617  ralsng  4614  dffun8  6520  ordiso2  9427  ordtypelem7  9436  cantnf  9612  rankonidlem  9750  dfac12lem3  10066  dcomex  10367  indstr2  12875  dfgcd2  16513  lublecllem  18322  tsmsgsum  24129  tsmsres  24134  tsmsxplem1  24143  caucfil  25275  isarchiofld  33287  mh-regprimbi  36780  wl-nfimf1  37904  tendoeq2  41273  naddgeoa  43846  elmapintrab  44027  inintabd  44030  cnvcnvintabd  44051  cnvintabd  44054  relexp0eq  44152  ntrkbimka  44489  ntrk0kbimka  44490  pm10.52  44816  ichnfimlem  47945  paireqne  47993