Theorem pm5.5 351

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  imim21b  382  dvelimdf  2335  2sb6rf  2452  elabgt  3347  sbceqal  3487  dffun8  5916  ordiso2  8420  ordtypelem7  8429  cantnf  8590  rankonidlem  8691  dfac12lem3  8967  dcomex  9269  indstr2  11767  dfgcd2  15263  lublecllem  16988  tsmsgsum  21942  tsmsres  21947  tsmsxplem1  21956  caucfil  23081  isarchiofld  29817  wl-nfimf1  33313  tendoeq2  36062  elmapintrab  37882  inintabd  37885  cnvcnvintabd  37906  cnvintabd  37909  relexp0eq  37993  ntrkbimka  38336  ntrk0kbimka  38337  pm10.52  38564