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

Theorem 3com13 1121
 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 1116 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp31 1109 1 ((𝜒𝜓𝜑) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  3comr  1122  3coml  1124  oacan  8159  oaword1  8163  nnacan  8239  nnaword1  8240  elmapg  8404  fisseneq  8715  ltapr  10458  subadd  10880  ltaddsub  11105  leaddsub  11107  iooshf  12806  faclbnd4  13655  relexpsucl  14384  relexpsucr  14385  dvdsmulc  15631  lcmdvdsb  15949  infpnlem1  16238  fmf  22557  frgr3v  28067  nvs  28453  dipdi  28633  dipsubdi  28639  spansncol  29358  chirredlem2  30181  mdsymlem3  30195  isbasisrelowllem2  34789  ltflcei  35061  iscringd  35452  resubadd  39532  iunrelexp0  40418  uun123p4  41533  isosctrlem1ALT  41655  stoweidlem17  42674
 Copyright terms: Public domain W3C validator