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

Theorem an12 644
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.) (Proof shortened by Peter Mazsa, 18-Sep-2022.)
Assertion
Ref Expression
an12 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))

Proof of Theorem an12
StepHypRef Expression
1 ancom 464 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
21bianass 641 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜒) ∧ 𝜓))
32biancomi 466 1 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  an12s  648  an4  655  3anan12  1093  ceqsrexv  3624  rmoan  3705  2reuswap  3712  2reuswap2  3713  reuxfrd  3714  reuind  3719  2rmoswap  3727  sbccomlem  3826  elunirab  4829  axsepgfromrep  5177  opeliunxp  5596  elinxp  5868  resoprab  7254  elrnmpores  7272  ov6g  7297  opabex3d  7652  opabex3rd  7653  opabex3  7654  dfrecs3  7996  oeeu  8216  xpassen  8598  omxpenlem  8605  dfac5lem2  9539  ltexprlem4  10450  2clim  14920  divalglem10  15742  bitsmod  15774  isssc  17081  eldmcoa  17316  issubrg  19526  isbasis2g  21551  tgval2  21559  is1stc2  22045  elflim2  22567  i1fres  24307  dvdsflsumcom  25771  vmasum  25798  logfac2  25799  axcontlem2  26757  fusgr2wsp2nb  28117  reuxfrdf  30260  1stpreima  30450  bnj849  32271  elima4  33093  elfuns  33450  dfrecs2  33485  dfrdg4  33486  bj-restuni  34473  bj-imdirco  34566  mptsnunlem  34716  relowlpssretop  34742  poimirlem27  35043  sstotbnd3  35173  an12i  35495  selconj  35497  eldmqsres  35662  inxpxrn  35762  rnxrnres  35766  refrelredund4  35989  islshpat  36272  islpln5  36790  islvol5  36834  cdleme0nex  37545  dicelval3  38435  mapdordlem1a  38889  2reuimp  43611  elpglem3  45182
  Copyright terms: Public domain W3C validator