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 1123 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 206  df-an 397  df-3an 1089
This theorem is referenced by:  3com12  1123  sotri3  6131  isinf  9259  isinfOLD  9260  infssuni  9342  fin1a2lem10  10403  elfz1b  13569  bernneq  14191  expnngt1  14203  swrdco  14787  dfgcd2  16487  lmodvsmmulgdi  20506  mamufacex  21890  gausslemma2dlem1a  26865  ssltun1  27306  ssltright  27363  upgrewlkle2  28860  pthdivtx  28983  clwwlkinwwlk  29290  upgr3v3e3cycl  29430  upgr4cycl4dv4e  29435  numclwwlk2lem1lem  29592  frgrregord013  29645  ax6e2ndeqALT  43682  fmtnofac2  46227
  Copyright terms: Public domain W3C validator