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  12942  dfgcd2  16594  lublecllem  18404  tsmsgsum  24257  tsmsres  24262  tsmsxplem1  24271  caucfil  25403  isarchiofld  33432  mh-regprimbi  36918  wl-nfimf1  38041  tendoeq2  41410  naddgeoa  43983  elmapintrab  44164  inintabd  44167  cnvcnvintabd  44188  cnvintabd  44191  relexp0eq  44289  ntrkbimka  44626  ntrk0kbimka  44627  pm10.52  44939  ichnfimlem  48067  paireqne  48115