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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.4  393  imbibi  396  imim21b  400  dvelimdf  2484  r19.35  3126  ceqsralv  3498  elabd2  3632  elabgt  3634  ralsng  4646  dffun8  6571  ordiso2  9487  ordtypelem7  9496  cantnf  9672  rankonidlem  9810  dfac12lem3  10148  dcomex  10449  indstr2  12969  dfgcd2  16629  lublecllem  18439  tsmsgsum  24333  tsmsres  24338  tsmsxplem1  24347  caucfil  25479  isarchiofld  33550  mh-regprimbi  37097  wl-nfimf1  38222  tendoeq2  41589  naddgeoa  44162  elmapintrab  44343  inintabd  44346  cnvcnvintabd  44367  cnvintabd  44370  relexp0eq  44468  ntrkbimka  44805  ntrk0kbimka  44806  pm10.52  45116  ichnfimlem  48253  paireqne  48301