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  2480  r19.35  3122  ceqsralv  3493  elabd2  3627  elabgt  3629  ralsng  4639  dffun8  6565  ordiso2  9491  ordtypelem7  9500  cantnf  9676  rankonidlem  9814  dfac12lem3  10152  dcomex  10453  indstr2  12980  dfgcd2  16642  lublecllem  18452  tsmsgsum  24371  tsmsres  24376  tsmsxplem1  24385  caucfil  25517  isarchiofld  33647  mh-regprimbi  37172  wl-nfimf1  38297  tendoeq2  41655  naddgeoa  44243  elmapintrab  44424  inintabd  44427  cnvcnvintabd  44448  cnvintabd  44451  relexp0eq  44549  ntrkbimka  44886  ntrk0kbimka  44887  pm10.52  45197  ichnfimlem  48371  paireqne  48419