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  2478  r19.35  3120  ceqsralv  3490  elabd2  3623  elabgt  3625  ralsng  4632  dffun8  6569  ordiso2  9513  ordtypelem7  9522  cantnf  9698  rankonidlem  9842  dfac12lem3  10228  dcomex  10529  indstr2  13058  dfgcd2  16725  lublecllem  18538  tsmsgsum  24464  tsmsres  24469  tsmsxplem1  24478  caucfil  25610  isarchiofld  33807  mh-regprimbi  37426  wl-nfimf1  38552  tendoeq2  41925  naddgeoa  44490  elmapintrab  44671  inintabd  44674  cnvcnvintabd  44694  cnvintabd  44697  relexp0eq  44795  ntrkbimka  45132  ntrk0kbimka  45133  pm10.52  45443  ichnfimlem  48639  paireqne  48687