Theorem pm5.5 364

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.4  393  imbibi  396  imim21b  400  dvelimdf  2479  r19.35  3121  ceqsralv  3491  elabd2  3624  elabgt  3626  ralsng  4636  dffun8  6560  ordiso2  9493  ordtypelem7  9502  cantnf  9678  rankonidlem  9819  dfac12lem3  10205  dcomex  10506  indstr2  13035  dfgcd2  16699  lublecllem  18512  tsmsgsum  24438  tsmsres  24443  tsmsxplem1  24452  caucfil  25584  isarchiofld  33742  mh-regprimbi  37303  wl-nfimf1  38426  tendoeq2  41799  naddgeoa  44354  elmapintrab  44535  inintabd  44538  cnvcnvintabd  44559  cnvintabd  44562  relexp0eq  44660  ntrkbimka  44997  ntrk0kbimka  44998  pm10.52  45308  ichnfimlem  48489  paireqne  48537