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

Theorem an4 799
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 774 . . 3  |-  ( ( ps  /\  ( ch 
/\  th ) )  <->  ( ch  /\  ( ps  /\  th ) ) )
21anbi2i 677 . 2  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
3 anass 632 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ph  /\  ( ps  /\  ( ch  /\  th ) ) ) )
4 anass 632 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
52, 3, 43bitr4i 270 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ( ph  /\  ch )  /\  ( ps  /\  th )
) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  an42  800  an4s  801  anandi  803  anandir  804  rnlem  933  an6  1264  2eu1  2363  2eu4  2366  reean  2876  reu2  3124  rmo4  3129  rmo3  3250  disjiun  4205  inxp  5010  xp11  5307  fununi  5520  fun  5610  resoprab2  6170  xporderlem  6460  poxp  6461  sorpsscmpl  6536  tfrlem7  6647  th3qlem1  7013  dfac5lem1  8009  zorn2lem6  8386  cju  10001  ixxin  10938  elfzo2  11148  summo  12516  gsumval3eu  15518  dvdsrtr  15762  isirred2  15811  lspsolvlem  16219  domnmuln0  16363  abvn0b  16367  unocv  16912  ordtrest2lem  17272  lmmo  17449  ptbasin  17614  txbasval  17643  txcnp  17657  txlm  17685  tx1stc  17687  tx2ndc  17688  isfild  17895  txflf  18043  mbfi1flimlem  19617  iblcnlem1  19682  iblre  19688  iblcn  19693  pf1ind  19980  logfaclbnd  21011  ocsh  22790  pjhthmo  22809  5oalem6  23166  cvnbtwn4  23797  superpos  23862  cdj3i  23949  rmo3f  23987  rmo4fOLD  23988  prodmo  25267  dfpo2  25383  poseq  25533  axcontlem4  25911  axcontlem7  25914  lineext  26015  outsideoftr  26068  hilbert1.2  26094  lineintmo  26096  ismblfin  26259  neibastop1  26402  unirep  26428  inixp  26444  ablo4pnp  26569  keridl  26656  ispridlc  26694  an43OLD  26710  prtlem70  26712  pell1234qrmulcl  26932  issubmd  27374  isdomn3  27514  2reu1  27954  2reu4a  27957  lcvbr3  29895  cvrnbtwn4  30151  linepsubN  30623  pmapsub  30639  pmapjoin  30723  ltrnu  30992  diblsmopel  32043
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 179  df-an 362
  Copyright terms: Public domain W3C validator