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  2484  r19.35  3126  ceqsralv  3498  elabd2  3632  elabgt  3634  ralsng  4644  dffun8  6568  ordiso2  9479  ordtypelem7  9488  cantnf  9664  rankonidlem  9802  dfac12lem3  10140  dcomex  10441  indstr2  12961  dfgcd2  16614  lublecllem  18424  tsmsgsum  24311  tsmsres  24316  tsmsxplem1  24325  caucfil  25457  isarchiofld  33532  mh-regprimbi  37088  wl-nfimf1  38213  tendoeq2  41580  naddgeoa  44153  elmapintrab  44334  inintabd  44337  cnvcnvintabd  44358  cnvintabd  44361  relexp0eq  44459  ntrkbimka  44796  ntrk0kbimka  44797  pm10.52  45107  ichnfimlem  48244  paireqne  48292