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

Theorem 3com13 1119
 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 1104 1 ((𝜒𝜓𝜑) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1072 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 197  df-an 385  df-3an 1074 This theorem is referenced by:  3comr  1120  3coml  1122  3adant3lOLD  1195  3adant3rOLD  1197  syld3an1OLD  1518  oacan  7797  oaword1  7801  nnacan  7877  nnaword1  7878  elmapg  8036  fisseneq  8336  ltapr  10059  subadd  10476  ltaddsub  10694  leaddsub  10696  iooshf  12445  faclbnd4  13278  relexpsucr  13968  relexpsucl  13972  dvdsmulc  15211  lcmdvdsb  15528  infpnlem1  15816  fmf  21950  frgr3v  27429  nvs  27827  dipdi  28007  dipsubdi  28013  spansncol  28736  chirredlem2  29559  mdsymlem3  29573  isbasisrelowllem2  33515  ltflcei  33710  iscringd  34110  iunrelexp0  38496  uun123p4  39541  isosctrlem1ALT  39669  stoweidlem17  40737
 Copyright terms: Public domain W3C validator