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

Theorem 3com13 1125
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3com13 ((𝜒𝜓𝜑) → 𝜃)

Proof of Theorem 3com13
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1120 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp31 1113 1 ((𝜒𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  3comr  1126  3coml  1128  oacan  8499  oaword1  8503  nnacan  8579  nnaword1  8580  elmapg  8784  fisseneq  9207  ltapr  10989  subadd  11412  ltaddsub  11637  leaddsub  11639  iooshf  13352  faclbnd4  14206  relexpsucl  14925  relexpsucr  14926  dvdsmulc  16174  lcmdvdsb  16497  infpnlem1  16790  fmf  23319  frgr3v  29268  nvs  29654  dipdi  29834  dipsubdi  29840  spansncol  30559  chirredlem2  31382  mdsymlem3  31396  isbasisrelowllem2  35877  ltflcei  36116  iscringd  36507  resubadd  40895  iunrelexp0  42066  uun123p4  43186  isosctrlem1ALT  43308  stoweidlem17  44348
  Copyright terms: Public domain W3C validator