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

Theorem 3com13 1158
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 1152 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp31 1143 1 ((𝜒𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1111
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 199  df-an 387  df-3an 1113
This theorem is referenced by:  3comr  1159  3coml  1161  3adant3lOLD  1234  3adant3rOLD  1236  syld3an1OLD  1534  oacan  7895  oaword1  7899  nnacan  7975  nnaword1  7976  elmapg  8135  fisseneq  8440  ltapr  10182  subadd  10604  ltaddsub  10826  leaddsub  10828  iooshf  12540  faclbnd4  13377  relexpsucr  14146  relexpsucl  14150  dvdsmulc  15386  lcmdvdsb  15699  infpnlem1  15985  fmf  22119  frgr3v  27645  nvs  28062  dipdi  28242  dipsubdi  28248  spansncol  28971  chirredlem2  29794  mdsymlem3  29808  isbasisrelowllem2  33742  ltflcei  33933  iscringd  34332  resubadd  38077  iunrelexp0  38828  uun123p4  39859  isosctrlem1ALT  39981  stoweidlem17  41021
  Copyright terms: Public domain W3C validator