Theorem pm5.5 365

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 364	. 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  393  imim21b  398  dvelimdf  2448  nfabdwOLD  2928  ceqsalv  3443  ceqsralv  3445  elabd2  3579  elabgtOLD  3582  elabg  3585  sbceqalOLD  3762  ralsng  4589  dffun8  6408  ordiso2  9131  ordtypelem7  9140  cantnf  9308  rankonidlem  9444  dfac12lem3  9759  dcomex  10061  indstr2  12523  dfgcd2  16106  lublecllem  17866  tsmsgsum  23036  tsmsres  23041  tsmsxplem1  23050  caucfil  24180  isarchiofld  31235  wl-nfimf1  35422  tendoeq2  38525  elmapintrab  40860  inintabd  40863  cnvcnvintabd  40884  cnvintabd  40887  relexp0eq  40986  ntrkbimka  41325  ntrk0kbimka  41326  pm10.52  41656  ichnfimlem  44588  paireqne  44636