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 1258  sbcom2 1334  mo 1393  2mo 1447  r19.21t 1715  reu8 1936  ra5 2000  unissb 2528  fun11 3562  oeordi 4214  oaabs 4252  aceq1 4729  primet 6195  raluz2 6443  metcnplem 7886  chcmh 9113  elat2 10267

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