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

Theorem 3com13 1262
 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 1042 . 2 ((𝜒𝜓𝜑) ↔ (𝜑𝜓𝜒))
2 3exp.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2sylbi 206 1 ((𝜒𝜓𝜑) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1031 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  df-3an 1033 This theorem is referenced by:  3coml  1264  3adant3l  1314  3adant3r  1315  syld3an1  1364  oacan  7515  oaword1  7519  nnacan  7595  nnaword1  7596  elmapg  7757  fisseneq  8056  ltapr  9746  subadd  10163  ltaddsub  10381  leaddsub  10383  iooshf  12123  faclbnd4  12946  relexpsucr  13617  relexpsucl  13621  dvdsmulc  14847  lcmdvdsb  15164  infpnlem1  15452  fmf  21559  frgra3v  26529  nvs  26902  dipdi  27082  dipsubdi  27088  spansncol  27811  chirredlem2  28634  mdsymlem3  28648  isbasisrelowllem2  32380  ltflcei  32567  iscringd  32967  iunrelexp0  37013  uun123p4  38060  isosctrlem1ALT  38192  stoweidlem17  38910  frgr3v  41445
 Copyright terms: Public domain W3C validator