Theorem bi2.04 160

Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122.

Assertion

Ref	Expression
bi2.04	|- ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))

Proof of Theorem bi2.04

Step	Hyp	Ref	Expression
1		pm2.04 30	. 2 |- ((ph -> (ps -> ch)) -> (ps -> (ph -> ch)))
2		pm2.04 30	. 2 |- ((ps -> (ph -> ch)) -> (ph -> (ps -> ch)))
3	1, 2	impbi 157	1 |- ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  or12 258  pm4.14 352  pm4.78 354  pm4.87 356  sbcom 1253  sbcom2 1329  mo 1386  2mo 1440  r19.21t 1707  reu8 1926  ra5 1990  unissb 2518  fun11 3548  oeordi 4198  oaabs 4236  aceq1 4701  primet 6142  raluz2 6375  metcnplem 7825  chcmh 9034  elat2 10175

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain