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

Theorem an12 795
Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
an12  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )

Proof of Theorem an12
StepHypRef Expression
1 ancom 450 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 695 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 649 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 649 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 275 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  an32  796  an13  797  an12s  799  an4  822  ceqsrexv  3217  rmoan  3282  2reuswap  3286  reuind  3287  sbccomlem  3390  elunirab  4243  axsep  4554  reuxfr2d  4657  opeliunxp  5038  elres  5296  resoprab  6380  elrnmpt2res  6398  ov6g  6422  opabex3d  6760  opabex3  6761  oeeu  7251  xpassen  7610  omxpenlem  7617  dfac5lem2  8505  ltexprlem4  9417  rexuz2  11138  wrdeqswrdlsw  12650  2clim  13371  divalglem10  13934  bitsmod  13960  isssc  15063  eldmcoa  15263  issubrg  17300  isbasis2g  19319  tgval2  19327  is1stc2  19813  elflim2  20335  i1fres  21982  dvdsflsumcom  23333  vmasum  23360  logfac2  23361  axcontlem2  24137  2reuswap2  27256  reuxfr3d  27257  1stpreima  27393  elima4  29181  nofulllem5  29438  elfuns  29537  brimg  29559  dfrdg4  29572  tfrqfree  29573  sstotbnd3  30244  an12i  30470  selconj  30472  2rmoswap  32027  bnj849  33711  bj-axsep  34112  islshpat  34465  islpln5  34982  islvol5  35026  cdleme0nex  35738  dicelval3  36630  mapdordlem1a  37084
  Copyright terms: Public domain W3C validator