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  2454  r19.35  3096  ceqsralv  3471  elabd2  3613  elabgt  3615  ralsng  4620  dffun8  6520  ordiso2  9423  ordtypelem7  9432  cantnf  9605  rankonidlem  9743  dfac12lem3  10059  dcomex  10360  indstr2  12868  dfgcd2  16506  lublecllem  18315  tsmsgsum  24114  tsmsres  24119  tsmsxplem1  24128  caucfil  25260  isarchiofld  33275  mh-regprimbi  36743  wl-nfimf1  37865  tendoeq2  41234  naddgeoa  43840  elmapintrab  44021  inintabd  44024  cnvcnvintabd  44045  cnvintabd  44048  relexp0eq  44146  ntrkbimka  44483  ntrk0kbimka  44484  pm10.52  44810  ichnfimlem  47935  paireqne  47983