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  2453  r19.35  3094  ceqsralv  3481  elabd2  3624  elabgt  3626  ralsng  4632  dffun8  6520  ordiso2  9420  ordtypelem7  9429  cantnf  9602  rankonidlem  9740  dfac12lem3  10056  dcomex  10357  indstr2  12840  dfgcd2  16473  lublecllem  18281  tsmsgsum  24083  tsmsres  24088  tsmsxplem1  24097  caucfil  25239  isarchiofld  33281  wl-nfimf1  37731  tendoeq2  41034  naddgeoa  43636  elmapintrab  43817  inintabd  43820  cnvcnvintabd  43841  cnvintabd  43844  relexp0eq  43942  ntrkbimka  44279  ntrk0kbimka  44280  pm10.52  44606  ichnfimlem  47709  paireqne  47757