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  2447  r19.35  3088  ceqsralv  3488  elabd2  3636  elabgt  3638  ralsng  4639  dffun8  6544  ordiso2  9468  ordtypelem7  9477  cantnf  9646  rankonidlem  9781  dfac12lem3  10099  dcomex  10400  indstr2  12886  dfgcd2  16516  lublecllem  18319  tsmsgsum  24026  tsmsres  24031  tsmsxplem1  24040  caucfil  25183  isarchiofld  33295  wl-nfimf1  37514  tendoeq2  40768  naddgeoa  43383  elmapintrab  43565  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  relexp0eq  43690  ntrkbimka  44027  ntrk0kbimka  44028  pm10.52  44354  ichnfimlem  47464  paireqne  47512