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

Theorem 3com13 1116
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 1111 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp31 1104 1 ((𝜒𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3comr  1117  3coml  1119  oacan  8163  oaword1  8167  nnacan  8243  nnaword1  8244  elmapg  8408  fisseneq  8717  ltapr  10455  subadd  10877  ltaddsub  11102  leaddsub  11104  iooshf  12803  faclbnd4  13645  relexpsucr  14376  relexpsucl  14380  dvdsmulc  15625  lcmdvdsb  15945  infpnlem1  16234  fmf  22481  frgr3v  27981  nvs  28367  dipdi  28547  dipsubdi  28553  spansncol  29272  chirredlem2  30095  mdsymlem3  30109  isbasisrelowllem2  34519  ltflcei  34761  iscringd  35157  resubadd  39087  iunrelexp0  39925  uun123p4  41023  isosctrlem1ALT  41145  stoweidlem17  42179
  Copyright terms: Public domain W3C validator