ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bi2.04 Unicode version

Theorem bi2.04 246
Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
bi2.04  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )

Proof of Theorem bi2.04
StepHypRef Expression
1 pm2.04 81 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  ( ps  ->  ( ph  ->  ch ) ) )
2 pm2.04 81 . 2  |-  ( ( ps  ->  ( ph  ->  ch ) )  -> 
( ph  ->  ( ps 
->  ch ) ) )
31, 2impbii 124 1  |-  ( (
ph  ->  ( ps  ->  ch ) )  <->  ( ps  ->  ( ph  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imim21b  250  pm4.87  524  imimorbdc  833  sbcom2v  1909  mor  1990  r19.21t  2448  reu8  2811  ra5  2927  unissb  3683  reusv3  4282  zfregfr  4389  tfi  4397  fun11  5081  prime  8843  raluz2  9065  isprm3  11374  isprm4  11375  bj-inf2vnlem2  11821
  Copyright terms: Public domain W3C validator