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

Theorem 3com13 1124
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 1119 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp31 1112 1 ((𝜒𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  3comr  1125  3coml  1127  oacan  8487  oaword1  8491  nnacan  8567  nnaword1  8568  elmapg  8736  fisseneq  9159  ltapr  10939  subadd  11362  ltaddsub  11587  leaddsub  11589  iooshf  13297  faclbnd4  14151  relexpsucl  14876  relexpsucr  14877  dvdsmulc  16126  lcmdvdsb  16449  infpnlem1  16742  fmf  23248  frgr3v  29048  nvs  29434  dipdi  29614  dipsubdi  29620  spansncol  30339  chirredlem2  31162  mdsymlem3  31176  isbasisrelowllem2  35765  ltflcei  36004  iscringd  36395  resubadd  40757  iunrelexp0  41885  uun123p4  43005  isosctrlem1ALT  43127  stoweidlem17  44159
  Copyright terms: Public domain W3C validator