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

Theorem an4 560
Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
Assertion
Ref Expression
an4  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ( ph  /\  ch )  /\  ( ps  /\  th )
) )

Proof of Theorem an4
StepHypRef Expression
1 an12 535 . . 3  |-  ( ( ps  /\  ( ch 
/\  th ) )  <->  ( ch  /\  ( ps  /\  th ) ) )
21anbi2i 452 . 2  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
3 anass 398 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ph  /\  ( ps  /\  ( ch  /\  th ) ) ) )
4 anass 398 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
52, 3, 43bitr4i 211 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ( ph  /\  ch )  /\  ( ps  /\  th )
) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  an42  561  an4s  562  anandi  564  anandir  565  rnlem  945  an6  1284  2eu4  2070  reean  2576  reu2  2845  rmo4  2850  rmo3f  2854  rmo3  2972  inxp  4643  xp11m  4947  fununi  5161  fun  5265  resoprab2  5836  xporderlem  6096  poxp  6097  th3qlem1  6499  enq0enq  7207  enq0tr  7210  genpdisj  7299  cju  8687  elfzo2  9895  iooinsup  11014  summodc  11120  txbasval  12363  txcnp  12367  txlm  12375
  Copyright terms: Public domain W3C validator