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

Theorem an4 824
Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
Assertion
Ref Expression
an4

Proof of Theorem an4
StepHypRef Expression
1 an12 797 . . 3
21anbi2i 694 . 2
3 anass 649 . 2
4 anass 649 . 2
52, 3, 43bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  an42  825  an4s  826  anandi  828  anandir  829  rnlemOLD  965  an6  1308  an33rean  1342  2eu1OLD  2377  2eu4OLD  2381  reean  3024  reu2  3287  rmo4  3292  rmo3  3429  disjiun  4442  inxp  5140  xp11  5447  fununi  5659  fun  5753  resoprab2  6399  sorpsscmpl  6591  xporderlem  6911  poxp  6912  dfac5lem1  8525  zorn2lem6  8902  cju  10557  ixxin  11575  elfzo2  11832  summo  13539  prodmo  13743  issubmd  15980  gsumval3eu  16907  dvdsrtr  17301  isirred2  17350  lspsolvlem  17788  domnmuln0  17947  abvn0b  17951  pf1ind  18391  unocv  18711  ordtrest2lem  19704  lmmo  19881  ptbasin  20078  txbasval  20107  txcnp  20121  txlm  20149  tx1stc  20151  tx2ndc  20152  isfild  20359  txflf  20507  mbfi1flimlem  22129  iblcnlem1  22194  iblre  22200  iblcn  22205  logfaclbnd  23497  axcontlem4  24270  axcontlem7  24273  ocsh  26201  pjhthmo  26220  5oalem6  26577  cvnbtwn4  27208  superpos  27273  cdj3i  27360  rmo3f  27394  rmo4fOLD  27395  ordtrest2NEWlem  27904  dfpo2  29184  poseq  29333  lineext  29726  outsideoftr  29779  hilbert1.2  29805  lineintmo  29807  ptrest  30048  ismblfin  30055  neibastop1  30177  unirep  30203  inixp  30219  ablo4pnp  30342  keridl  30429  ispridlc  30467  an43OLD  30590  prtlem70  30592  pell1234qrmulcl  30791  isdomn3  31164  2reu1  32191  2reu4a  32194  dfiso2  32568  bj-inrab  34495  lcvbr3  34748  cvrnbtwn4  35004  linepsubN  35476  pmapsub  35492  pmapjoin  35576  ltrnu  35845  diblsmopel  36898  bj-ifidg  37707  bj-ifbibib  37721  bj-ifan23  37729  xpcogend  37773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator