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

Theorem 3com13 1261
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com13 ((𝜒𝜓𝜑) → 𝜃)

Proof of Theorem 3com13
StepHypRef Expression
1 3anrev 1041 . 2 ((𝜒𝜓𝜑) ↔ (𝜑𝜓𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbi 205 1 ((𝜒𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3coml  1263  3adant3l  1313  3adant3r  1314  syld3an1  1363  oacan  7489  oaword1  7493  nnacan  7569  nnaword1  7570  elmapg  7731  fisseneq  8030  ltapr  9720  subadd  10132  ltaddsub  10348  leaddsub  10350  iooshf  12076  faclbnd4  12898  relexpsucr  13560  relexpsucl  13564  dvdsmulc  14790  lcmdvdsb  15107  infpnlem1  15395  fmf  21498  frgra3v  26292  nvs  26692  dipdi  26885  dipsubdi  26891  spansncol  27614  chirredlem2  28437  mdsymlem3  28451  isbasisrelowllem2  32180  ltflcei  32367  iscringd  32767  iunrelexp0  36813  uun123p4  37860  isosctrlem1ALT  37992  stoweidlem17  38711  frgr3v  41444
  Copyright terms: Public domain W3C validator