Theorem pm5.5 364

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  pm5.4  392  imim21b  397  dvelimdf  2471  nfabdw  3000  elabgt  3663  sbceqal  3835  dffun8  6383  ordiso2  8979  ordtypelem7  8988  cantnf  9156  rankonidlem  9257  dfac12lem3  9571  dcomex  9869  indstr2  12328  dfgcd2  15894  lublecllem  17598  tsmsgsum  22747  tsmsres  22752  tsmsxplem1  22761  caucfil  23886  isarchiofld  30890  wl-nfimf1  34781  tendoeq2  37925  elmapintrab  39956  inintabd  39959  cnvcnvintabd  39980  cnvintabd  39983  relexp0eq  40066  ntrkbimka  40408  ntrk0kbimka  40409  pm10.52  40717  paireqne  43693