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

Theorem 3com13 1118
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 1113 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp31 1106 1 ((𝜒𝜓𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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 1083
This theorem is referenced by:  3comr  1119  3coml  1121  oacan  8167  oaword1  8171  nnacan  8247  nnaword1  8248  elmapg  8412  fisseneq  8721  ltapr  10459  subadd  10881  ltaddsub  11106  leaddsub  11108  iooshf  12808  faclbnd4  13650  relexpsucr  14381  relexpsucl  14385  dvdsmulc  15629  lcmdvdsb  15949  infpnlem1  16238  fmf  22469  frgr3v  27969  nvs  28355  dipdi  28535  dipsubdi  28541  spansncol  29260  chirredlem2  30083  mdsymlem3  30097  isbasisrelowllem2  34507  ltflcei  34748  iscringd  35145  resubadd  39073  iunrelexp0  39909  uun123p4  41008  isosctrlem1ALT  41130  stoweidlem17  42165
  Copyright terms: Public domain W3C validator