Theorem pm5.5 350

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 349	. 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  381  dvelimdf  2366  2sb6rf  2480  elabgt  3379  sbceqal  3520  dffun8  5954  ordiso2  8461  ordtypelem7  8470  cantnf  8628  rankonidlem  8729  dfac12lem3  9005  dcomex  9307  indstr2  11805  dfgcd2  15310  lublecllem  17035  tsmsgsum  21989  tsmsres  21994  tsmsxplem1  22003  caucfil  23127  isarchiofld  29945  wl-nfimf1  33443  tendoeq2  36379  elmapintrab  38199  inintabd  38202  cnvcnvintabd  38223  cnvintabd  38226  relexp0eq  38310  ntrkbimka  38653  ntrk0kbimka  38654  pm10.52  38881