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

Theorem an4 797
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 772 . . 3  |-  ( ( ps  /\  ( ch 
/\  th ) )  <->  ( ch  /\  ( ps  /\  th ) ) )
21anbi2i 675 . 2  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
3 anass 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ph  /\  ( ps  /\  ( ch  /\  th ) ) ) )
4 anass 630 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ph  /\  ( ch  /\  ( ps  /\  th ) ) ) )
52, 3, 43bitr4i 268 1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  <->  ( ( ph  /\  ch )  /\  ( ps  /\  th )
) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  an42  798  an4s  799  anandi  801  anandir  802  rnlem  931  an6  1261  2eu1  2223  2eu4  2226  reean  2706  reu2  2953  rmo4  2958  rmo3  3078  disjiun  4013  inxp  4818  xp11  5111  fununi  5316  fun  5405  resoprab2  5941  xporderlem  6226  poxp  6227  sorpsscmpl  6288  tfrlem7  6399  th3qlem1  6764  dfac5lem1  7750  zorn2lem6  8128  cju  9742  ixxin  10673  elfzo2  10878  summo  12190  gsumval3eu  15190  dvdsrtr  15434  isirred2  15483  lspsolvlem  15895  domnmuln0  16039  abvn0b  16043  unocv  16580  ordtrest2lem  16933  lmmo  17108  ptbasin  17272  txbasval  17301  txcnp  17314  txlm  17342  tx1stc  17344  tx2ndc  17345  isfild  17553  txflf  17701  mbfi1flimlem  19077  iblcnlem1  19142  iblre  19148  iblcn  19153  pf1ind  19438  logfaclbnd  20461  ocsh  21862  pjhthmo  21881  5oalem6  22238  cvnbtwn4  22869  superpos  22934  cdj3i  23021  rmo3f  23178  rmo4fOLD  23179  dfpo2  24112  poseq  24253  axcontlem4  24595  axcontlem7  24598  lineext  24699  outsideoftr  24752  hilbert1.2  24778  lineintmo  24780  qusp  25542  limptlimpr2lem1  25574  neibastop1  26308  unirep  26349  inixp  26399  ablo4pnp  26570  keridl  26657  ispridlc  26695  an43OLD  26713  prtlem70  26715  pell1234qrmulcl  26940  issubmd  27383  isdomn3  27523  2reu1  27964  2reu4a  27967  lcvbr3  29213  cvrnbtwn4  29469  linepsubN  29941  pmapsub  29957  pmapjoin  30041  ltrnu  30310  diblsmopel  31361
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 177  df-an 360
  Copyright terms: Public domain W3C validator