Theorem pm5.5 363

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 362	. 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  391  imbibi  394  imim21b  398  dvelimdf  2479  r19.35  3119  ceqsralv  3493  elabd2  3629  elabgt  3631  ralsng  4633  dffun8  6545  ordiso2  9460  ordtypelem7  9469  cantnf  9645  rankonidlem  9783  dfac12lem3  10099  dcomex  10401  indstr2  12925  dfgcd2  16563  lublecllem  18373  tsmsgsum  24179  tsmsres  24184  tsmsxplem1  24193  caucfil  25325  isarchiofld  33340  mh-regprimbi  36869  wl-nfimf1  37993  tendoeq2  41362  naddgeoa  43935  elmapintrab  44116  inintabd  44119  cnvcnvintabd  44140  cnvintabd  44143  relexp0eq  44241  ntrkbimka  44578  ntrk0kbimka  44579  pm10.52  44905  ichnfimlem  48033  paireqne  48081