Theorem pm5.5 361

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pm5.4  389  imim21b  395  dvelimdf  2447  nfabdwOLD  2926  r19.35  3107  ceqsralv  3511  elabd2  3656  elabgtOLD  3659  elabg  3662  sbceqalOLD  3840  ralsng  4670  dffun8  6565  ordiso2  9492  ordtypelem7  9501  cantnf  9670  rankonidlem  9805  dfac12lem3  10122  dcomex  10424  indstr2  12893  dfgcd2  16470  lublecllem  18295  tsmsgsum  23572  tsmsres  23577  tsmsxplem1  23586  caucfil  24729  isarchiofld  32297  wl-nfimf1  36197  tendoeq2  39448  naddgeoa  41914  elmapintrab  42096  inintabd  42099  cnvcnvintabd  42120  cnvintabd  42123  relexp0eq  42221  ntrkbimka  42558  ntrk0kbimka  42559  pm10.52  42893  ichnfimlem  45901  paireqne  45949