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  2289  2eu4  2292  reean  2782  reu2  3029  rmo4  3034  rmo3  3154  disjiun  4092  inxp  4897  xp11  5190  fununi  5395  fun  5485  resoprab2  6025  xporderlem  6310  poxp  6311  sorpsscmpl  6372  tfrlem7  6483  th3qlem1  6849  dfac5lem1  7837  zorn2lem6  8215  cju  9829  ixxin  10762  elfzo2  10967  summo  12281  gsumval3eu  15283  dvdsrtr  15527  isirred2  15576  lspsolvlem  15988  domnmuln0  16132  abvn0b  16136  unocv  16680  ordtrest2lem  17033  lmmo  17208  ptbasin  17372  txbasval  17401  txcnp  17414  txlm  17442  tx1stc  17444  tx2ndc  17445  isfild  17649  txflf  17797  mbfi1flimlem  19175  iblcnlem1  19240  iblre  19246  iblcn  19251  pf1ind  19536  logfaclbnd  20567  ocsh  21970  pjhthmo  21989  5oalem6  22346  cvnbtwn4  22977  superpos  23042  cdj3i  23129  rmo3f  23171  rmo4fOLD  23172  prodmo  24563  dfpo2  24670  poseq  24811  axcontlem4  25154  axcontlem7  25157  lineext  25258  outsideoftr  25311  hilbert1.2  25337  lineintmo  25339  neibastop1  25632  unirep  25673  inixp  25723  ablo4pnp  25893  keridl  25980  ispridlc  26018  an43OLD  26036  prtlem70  26038  pell1234qrmulcl  26263  issubmd  26706  isdomn3  26846  2reu1  27287  2reu4a  27290  lcvbr3  29265  cvrnbtwn4  29521  linepsubN  29993  pmapsub  30009  pmapjoin  30093  ltrnu  30362  diblsmopel  31413
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