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

Theorem 3imp21 1114
Description: The importation inference 3imp 1111 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 1124 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 1113 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  3com12  1124  sotri3  6150  isinf  9296  isinfOLD  9297  infssuni  9386  fin1a2lem10  10449  elfz1b  13633  bernneq  14268  expnngt1  14280  swrdco  14876  dfgcd2  16583  lmodvsmmulgdi  20895  mamufacex  22400  gausslemma2dlem1a  27409  ssltun1  27853  ssltright  27910  expsgt0  28415  upgrewlkle2  29624  pthdivtx  29747  clwwlkinwwlk  30059  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  numclwwlk2lem1lem  30361  frgrregord013  30414  ax6e2ndeqALT  44951  fmtnofac2  47556
  Copyright terms: Public domain W3C validator