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

Theorem an12 834
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 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))

Proof of Theorem an12
StepHypRef Expression
1 ancom 465 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
21anbi1i 727 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 anass 679 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
4 anass 679 . 2 (((𝜓𝜑) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
52, 3, 43bitr3i 289 1 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  an32  835  an13  836  an12s  839  an4  861  ceqsrexv  3306  rmoan  3373  2reuswap  3377  reuind  3378  sbccomlem  3475  elunirab  4384  axsep  4708  reuxfr2d  4817  opeliunxp  5093  elres  5355  resoprab  6654  elrnmpt2res  6672  ov6g  6696  opabex3d  7037  opabex3  7038  dfrecs3  7356  oeeu  7570  xpassen  7939  omxpenlem  7946  dfac5lem2  8830  ltexprlem4  9740  rexuz2  11615  2clim  14151  divalglem10  14963  bitsmod  14996  isssc  16303  eldmcoa  16538  issubrg  18603  isbasis2g  20563  tgval2  20571  is1stc2  21055  elflim2  21578  i1fres  23278  dvdsflsumcom  24714  vmasum  24741  logfac2  24742  axcontlem2  25645  2reuswap2  28712  reuxfr3d  28713  1stpreima  28867  bnj849  30249  elima4  30924  nofulllem5  31105  elfuns  31192  brimg  31214  dfrecs2  31227  dfrdg4  31228  bj-axsep  31981  bj-restuni  32231  mptsnunlem  32361  relowlpssretop  32388  poimirlem27  32606  sstotbnd3  32745  an12i  33070  selconj  33072  islshpat  33322  islpln5  33839  islvol5  33883  cdleme0nex  34595  dicelval3  35487  mapdordlem1a  35941  2rmoswap  39833  elpglem3  42255
  Copyright terms: Public domain W3C validator