Theorem pm5.5 362

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 361	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
2	1	bicomd 222	1 ⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pm5.4  390  imim21b  395  dvelimdf  2449  nfabdwOLD  2931  ceqsalv  3467  ceqsralv  3469  elabd2  3601  elabgtOLD  3604  elabg  3607  sbceqalOLD  3783  ralsng  4609  dffun8  6462  ordiso2  9274  ordtypelem7  9283  cantnf  9451  rankonidlem  9586  dfac12lem3  9901  dcomex  10203  indstr2  12667  dfgcd2  16254  lublecllem  18078  tsmsgsum  23290  tsmsres  23295  tsmsxplem1  23304  caucfil  24447  isarchiofld  31516  wl-nfimf1  35685  tendoeq2  38788  elmapintrab  41184  inintabd  41187  cnvcnvintabd  41208  cnvintabd  41211  relexp0eq  41309  ntrkbimka  41648  ntrk0kbimka  41649  pm10.52  41983  ichnfimlem  44915  paireqne  44963