MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an4 Unicode version

Theorem an4 798
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 773 . . 3  |-  ( ( ps  /\  ( ch 
/\  th ) )  <->  ( ch  /\  ( ps  /\  th ) ) )
21anbi2i 676 . 2  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
3 anass 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ph  /\  ( ps  /\  ( ch  /\  th ) ) ) )
4 anass 631 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
52, 3, 43bitr4i 269 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ( ph  /\  ch )  /\  ( ps  /\  th )
) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an42  799  an4s  800  anandi  802  anandir  803  rnlem  932  an6  1263  2eu1  2338  2eu4  2341  reean  2838  reu2  3086  rmo4  3091  rmo3  3212  disjiun  4166  inxp  4970  xp11  5267  fununi  5480  fun  5570  resoprab2  6130  xporderlem  6420  poxp  6421  sorpsscmpl  6496  tfrlem7  6607  th3qlem1  6973  dfac5lem1  7964  zorn2lem6  8341  cju  9956  ixxin  10893  elfzo2  11102  summo  12470  gsumval3eu  15472  dvdsrtr  15716  isirred2  15765  lspsolvlem  16173  domnmuln0  16317  abvn0b  16321  unocv  16866  ordtrest2lem  17225  lmmo  17402  ptbasin  17566  txbasval  17595  txcnp  17609  txlm  17637  tx1stc  17639  tx2ndc  17640  isfild  17847  txflf  17995  mbfi1flimlem  19571  iblcnlem1  19636  iblre  19642  iblcn  19647  pf1ind  19932  logfaclbnd  20963  ocsh  22742  pjhthmo  22761  5oalem6  23118  cvnbtwn4  23749  superpos  23814  cdj3i  23901  rmo3f  23939  rmo4fOLD  23940  prodmo  25219  dfpo2  25330  poseq  25471  axcontlem4  25814  axcontlem7  25817  lineext  25918  outsideoftr  25971  hilbert1.2  25997  lineintmo  25999  ismblfin  26150  neibastop1  26282  unirep  26308  inixp  26324  ablo4pnp  26449  keridl  26536  ispridlc  26574  an43OLD  26590  prtlem70  26592  pell1234qrmulcl  26812  issubmd  27255  isdomn3  27395  2reu1  27835  2reu4a  27838  lcvbr3  29510  cvrnbtwn4  29766  linepsubN  30238  pmapsub  30254  pmapjoin  30338  ltrnu  30607  diblsmopel  31658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator