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  2481  r19.35  3124  ceqsralv  3494  elabd2  3627  elabgt  3629  ralsng  4636  dffun8  6591  ordiso2  9539  ordtypelem7  9548  cantnf  9724  rankonidlem  9868  dfac12lem3  10254  dcomex  10555  indstr2  13084  dfgcd2  16751  lublecllem  18564  tsmsgsum  24491  tsmsres  24496  tsmsxplem1  24505  caucfil  25637  isarchiofld  33836  mh-regprimbi  37524  wl-nfimf1  38663  tendoeq2  42034  naddgeoa  44599  elmapintrab  44780  inintabd  44783  cnvcnvintabd  44803  cnvintabd  44806  relexp0eq  44904  ntrkbimka  45241  ntrk0kbimka  45242  pm10.52  45552  ichnfimlem  48760  paireqne  48808