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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  pm5.4  392  imim21b  397  dvelimdf  2470  nfabdw  3003  elabgt  3666  sbceqal  3838  dffun8  6386  ordiso2  8982  ordtypelem7  8991  cantnf  9159  rankonidlem  9260  dfac12lem3  9574  dcomex  9872  indstr2  12330  dfgcd2  15897  lublecllem  17601  tsmsgsum  22750  tsmsres  22755  tsmsxplem1  22764  caucfil  23889  isarchiofld  30894  wl-nfimf1  34770  tendoeq2  37914  elmapintrab  39942  inintabd  39945  cnvcnvintabd  39966  cnvintabd  39969  relexp0eq  40052  ntrkbimka  40394  ntrk0kbimka  40395  pm10.52  40703  paireqne  43680