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  396  dvelimdf  2449  nfabdwOLD  2928  r19.35  3109  ceqsralv  3514  elabd2  3661  elabgtOLD  3664  elabg  3667  sbceqalOLD  3845  ralsng  4678  dffun8  6577  ordiso2  9510  ordtypelem7  9519  cantnf  9688  rankonidlem  9823  dfac12lem3  10140  dcomex  10442  indstr2  12911  dfgcd2  16488  lublecllem  18313  tsmsgsum  23643  tsmsres  23648  tsmsxplem1  23657  caucfil  24800  isarchiofld  32435  wl-nfimf1  36395  tendoeq2  39645  naddgeoa  42145  elmapintrab  42327  inintabd  42330  cnvcnvintabd  42351  cnvintabd  42354  relexp0eq  42452  ntrkbimka  42789  ntrk0kbimka  42790  pm10.52  43124  ichnfimlem  46131  paireqne  46179