Theorem pm5.5 354

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  imim21b  386  dvelimdf  2386  2sb6rfOLD  2421  elabgt  3570  sbceqal  3731  dffun8  6213  ordiso2  8772  ordtypelem7  8781  cantnf  8948  rankonidlem  9049  dfac12lem3  9363  dcomex  9665  indstr2  12139  dfgcd2  15748  lublecllem  17468  tsmsgsum  22465  tsmsres  22470  tsmsxplem1  22479  caucfil  23604  isarchiofld  30601  wl-nfimf1  34246  tendoeq2  37392  elmapintrab  39336  inintabd  39339  cnvcnvintabd  39360  cnvintabd  39363  relexp0eq  39447  ntrkbimka  39789  ntrk0kbimka  39790  pm10.52  40151  paireqne  43073