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  2448  nfabdwOLD  2927  r19.35  3108  ceqsralv  3513  elabd2  3659  elabgtOLD  3662  elabg  3665  sbceqalOLD  3843  ralsng  4676  dffun8  6573  ordiso2  9506  ordtypelem7  9515  cantnf  9684  rankonidlem  9819  dfac12lem3  10136  dcomex  10438  indstr2  12907  dfgcd2  16484  lublecllem  18309  tsmsgsum  23634  tsmsres  23639  tsmsxplem1  23648  caucfil  24791  isarchiofld  32423  wl-nfimf1  36383  tendoeq2  39633  naddgeoa  42130  elmapintrab  42312  inintabd  42315  cnvcnvintabd  42336  cnvintabd  42339  relexp0eq  42437  ntrkbimka  42774  ntrk0kbimka  42775  pm10.52  43109  ichnfimlem  46117  paireqne  46165