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  2481  r19.35  3123  ceqsralv  3495  elabd2  3630  elabgt  3632  ralsng  4642  dffun8  6566  ordiso2  9478  ordtypelem7  9487  cantnf  9663  rankonidlem  9801  dfac12lem3  10130  dcomex  10432  indstr2  12952  dfgcd2  16605  lublecllem  18415  tsmsgsum  24277  tsmsres  24282  tsmsxplem1  24291  caucfil  25423  isarchiofld  33500  mh-regprimbi  37037  wl-nfimf1  38162  tendoeq2  41529  naddgeoa  44104  elmapintrab  44285  inintabd  44288  cnvcnvintabd  44309  cnvintabd  44312  relexp0eq  44410  ntrkbimka  44747  ntrk0kbimka  44748  pm10.52  45058  ichnfimlem  48195  paireqne  48243