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

Theorem an4 840
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 814 . . 3  |-  ( ( ps  /\  ( ch 
/\  th ) )  <->  ( ch  /\  ( ps  /\  th ) ) )
21anbi2i 708 . 2  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
3 anass 661 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ph  /\  ( ps  /\  ( ch  /\  th ) ) ) )
4 anass 661 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
52, 3, 43bitr4i 285 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ( ph  /\  ch )  /\  ( ps  /\  th )
) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  an42  841  an4s  842  anandi  844  anandir  845  an6  1374  an33rean  1411  reean  2943  reu2  3214  rmo4  3219  rmo3  3344  disjiun  4386  inxp  4972  xp11  5278  fununi  5659  fun  5758  resoprab2  6412  sorpsscmpl  6601  xporderlem  6926  poxp  6927  dfac5lem1  8572  zorn2lem6  8949  cju  10627  ixxin  11677  elfzo2  11950  xpcogend  13113  summo  13860  prodmo  14067  dfiso2  15755  issubmd  16674  gsumval3eu  17616  dvdsrtr  17958  isirred2  18007  lspsolvlem  18443  domnmuln0  18599  abvn0b  18603  pf1ind  19020  unocv  19320  ordtrest2lem  20296  lmmo  20473  ptbasin  20669  txbasval  20698  txcnp  20712  txlm  20740  tx1stc  20742  tx2ndc  20743  isfild  20951  txflf  21099  mbfi1flimlem  22759  iblcnlem1  22824  iblre  22830  iblcn  22835  logfaclbnd  24229  axcontlem4  25076  axcontlem7  25079  ocsh  27017  pjhthmo  27036  5oalem6  27393  cvnbtwn4  28023  superpos  28088  cdj3i  28175  rmo3f  28210  rmo4fOLD  28211  smatrcl  28696  ordtrest2NEWlem  28802  dfpo2  30466  poseq  30562  lineext  30914  outsideoftr  30967  hilbert1.2  30993  lineintmo  30995  neibastop1  31086  bj-inrab  31598  isbasisrelowllem1  31828  isbasisrelowllem2  31829  ptrest  32003  poimirlem26  32030  ismblfin  32045  unirep  32103  inixp  32119  ablo4pnp  32242  keridl  32329  ispridlc  32367  prtlem70  32489  lcvbr3  32660  cvrnbtwn4  32916  linepsubN  33388  pmapsub  33404  pmapjoin  33488  ltrnu  33757  diblsmopel  34810  pell1234qrmulcl  35772  isdomn3  36152  ifpan23  36174  ifpidg  36206  ifpbibib  36225  2reu1  38752  2reu4a  38755
  Copyright terms: Public domain W3C validator