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

Theorem 3imp21 1142
Description: The importation inference 3imp 1138 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) (Revised to shorten 3com12 1154 by Wolf Lammen, 23-Jun-2022.)
Hypothesis
Ref Expression
3imp.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
3imp21 ((𝜓𝜑𝜒) → 𝜃)

Proof of Theorem 3imp21
StepHypRef Expression
1 3imp.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com13 88 . 2 (𝜒 → (𝜓 → (𝜑𝜃)))
323imp231 1141 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  3com12  1154  sotri3  5742  elfz1b  12659  expnngt1  13278  gausslemma2dlem1a  25439  upgrewlkle2  26848  pthdivtx  26975  clwwlkinwwlk  27340  clwwlkinwwlkOLD  27341  clwlksfclwwlkOLD  27395  upgr3v3e3cycl  27516  upgr4cycl4dv4e  27521  numclwwlk2lem1lem  27684  frgrregord013  27772  ax6e2ndeqALT  39915  fmtnofac2  42251
  Copyright terms: Public domain W3C validator