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 ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  pm5.4  392  imbibi  395  imim21b  399  dvelimdf  2483  r19.35  3123  ceqsralv  3497  elabd2  3632  elabgt  3634  ralsng  4637  dffun8  6553  ordiso2  9465  ordtypelem7  9474  cantnf  9650  rankonidlem  9788  dfac12lem3  10117  dcomex  10419  indstr2  12939  dfgcd2  16592  lublecllem  18402  tsmsgsum  24253  tsmsres  24258  tsmsxplem1  24267  caucfil  25399  isarchiofld  33427  mh-regprimbi  36913  wl-nfimf1  38036  tendoeq2  41405  naddgeoa  43978  elmapintrab  44159  inintabd  44162  cnvcnvintabd  44183  cnvintabd  44186  relexp0eq  44284  ntrkbimka  44621  ntrk0kbimka  44622  pm10.52  44934  ichnfimlem  48068  paireqne  48116