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

Theorem 3imp21 1112
Description: The importation inference 3imp 1109 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 1121 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 1111 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1085
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 395  df-3an 1087
This theorem is referenced by:  3com12  1121  sotri3  6130  isinf  9262  isinfOLD  9263  infssuni  9345  fin1a2lem10  10406  elfz1b  13574  bernneq  14196  expnngt1  14208  swrdco  14792  dfgcd2  16492  lmodvsmmulgdi  20651  mamufacex  22111  gausslemma2dlem1a  27104  ssltun1  27546  ssltright  27603  upgrewlkle2  29130  pthdivtx  29253  clwwlkinwwlk  29560  upgr3v3e3cycl  29700  upgr4cycl4dv4e  29705  numclwwlk2lem1lem  29862  frgrregord013  29915  ax6e2ndeqALT  43994  fmtnofac2  46535
  Copyright terms: Public domain W3C validator