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

Theorem 3com13 1268
 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 1047 . 2 ((𝜒𝜓𝜑) ↔ (𝜑𝜓𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbi 207 1 ((𝜒𝜓𝜑) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1036 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 197  df-an 386  df-3an 1038 This theorem is referenced by:  3coml  1270  3adant3l  1320  3adant3r  1321  syld3an1  1370  oacan  7613  oaword1  7617  nnacan  7693  nnaword1  7694  elmapg  7855  fisseneq  8156  ltapr  9852  subadd  10269  ltaddsub  10487  leaddsub  10489  iooshf  12237  faclbnd4  13067  relexpsucr  13750  relexpsucl  13754  dvdsmulc  14990  lcmdvdsb  15307  infpnlem1  15595  fmf  21730  frgr3v  27119  nvs  27488  dipdi  27668  dipsubdi  27674  spansncol  28397  chirredlem2  29220  mdsymlem3  29234  isbasisrelowllem2  33175  ltflcei  33368  iscringd  33768  iunrelexp0  37813  uun123p4  38859  isosctrlem1ALT  38990  stoweidlem17  39997
 Copyright terms: Public domain W3C validator