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

Theorem an12 627
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 anass 456 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an21 626 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitr3i 268 1 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  an32  628  an13  629  an12s  631  an4  638  3anan12  1110  ceqsrexv  3541  rmoan  3615  2reuswap  3619  reuind  3620  sbccomlem  3715  elunirab  4653  axsep  4987  reuxfr2d  5101  opeliunxp  5384  elinxp  5651  elresOLD  5653  resoprab  6996  elrnmpt2res  7014  ov6g  7038  opabex3d  7385  opabex3  7386  dfrecs3  7715  oeeu  7930  xpassen  8303  omxpenlem  8310  dfac5lem2  9240  ltexprlem4  10156  rexuz2  11977  2clim  14546  divalglem10  15365  bitsmod  15397  isssc  16704  eldmcoa  16939  issubrg  19004  isbasis2g  20987  tgval2  20995  is1stc2  21480  elflim2  22002  i1fres  23709  dvdsflsumcom  25151  vmasum  25178  logfac2  25179  axcontlem2  26082  fusgr2wsp2nb  27532  2reuswap2  29677  reuxfr3d  29678  1stpreima  29834  bnj849  31340  elima4  32021  elfuns  32365  brimg  32387  dfrecs2  32400  dfrdg4  32401  bj-axsep  33126  bj-restuni  33380  mptsnunlem  33521  relowlpssretop  33547  poimirlem27  33768  sstotbnd3  33905  an12i  34230  selconj  34232  eldmqsres  34387  inxpxrn  34485  rnxrnres  34489  islshpat  34816  islpln5  35334  islvol5  35378  cdleme0nex  36089  dicelval3  36979  mapdordlem1a  37433  2rmoswap  41714  elpglem3  43045
  Copyright terms: Public domain W3C validator