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  2334  2eu4  2337  reean  2834  reu2  3082  rmo4  3087  rmo3  3208  disjiun  4162  inxp  4966  xp11  5263  fununi  5476  fun  5566  resoprab2  6126  xporderlem  6416  poxp  6417  sorpsscmpl  6492  tfrlem7  6603  th3qlem1  6969  dfac5lem1  7960  zorn2lem6  8337  cju  9952  ixxin  10889  elfzo2  11098  summo  12466  gsumval3eu  15468  dvdsrtr  15712  isirred2  15761  lspsolvlem  16169  domnmuln0  16313  abvn0b  16317  unocv  16862  ordtrest2lem  17221  lmmo  17398  ptbasin  17562  txbasval  17591  txcnp  17605  txlm  17633  tx1stc  17635  tx2ndc  17636  isfild  17843  txflf  17991  mbfi1flimlem  19567  iblcnlem1  19632  iblre  19638  iblcn  19643  pf1ind  19928  logfaclbnd  20959  ocsh  22738  pjhthmo  22757  5oalem6  23114  cvnbtwn4  23745  superpos  23810  cdj3i  23897  rmo3f  23935  rmo4fOLD  23936  prodmo  25215  dfpo2  25326  poseq  25467  axcontlem4  25810  axcontlem7  25813  lineext  25914  outsideoftr  25967  hilbert1.2  25993  lineintmo  25995  ismblfin  26146  neibastop1  26278  unirep  26304  inixp  26320  ablo4pnp  26445  keridl  26532  ispridlc  26570  an43OLD  26586  prtlem70  26588  pell1234qrmulcl  26808  issubmd  27251  isdomn3  27391  2reu1  27831  2reu4a  27834  lcvbr3  29506  cvrnbtwn4  29762  linepsubN  30234  pmapsub  30250  pmapjoin  30334  ltrnu  30603  diblsmopel  31654
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