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  8548  oaword1  8552  nnacan  8628  nnaword1  8629  elmapg  8833  fisseneq  9257  ltapr  11040  subadd  11463  ltaddsub  11688  leaddsub  11690  iooshf  13403  faclbnd4  14257  relexpsucl  14978  relexpsucr  14979  dvdsmulc  16227  lcmdvdsb  16550  infpnlem1  16843  fmf  23449  frgr3v  29559  nvs  29947  dipdi  30127  dipsubdi  30133  spansncol  30852  chirredlem2  31675  mdsymlem3  31689  isbasisrelowllem2  36285  ltflcei  36524  iscringd  36914  resubadd  41300  iunrelexp0  42501  uun123p4  43621  isosctrlem1ALT  43743  stoweidlem17  44781
  Copyright terms: Public domain W3C validator