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

Theorem 3imp21 1115
Description: The importation inference 3imp 1112 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 1114 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3com12  1124  sotri3  6088  isinf  9210  isinfOLD  9211  infssuni  9293  fin1a2lem10  10353  elfz1b  13519  bernneq  14141  expnngt1  14153  swrdco  14735  dfgcd2  16435  lmodvsmmulgdi  20401  mamufacex  21761  gausslemma2dlem1a  26736  ssltun1  27176  ssltright  27230  upgrewlkle2  28603  pthdivtx  28726  clwwlkinwwlk  29033  upgr3v3e3cycl  29173  upgr4cycl4dv4e  29178  numclwwlk2lem1lem  29335  frgrregord013  29388  ax6e2ndeqALT  43305  fmtnofac2  45851
  Copyright terms: Public domain W3C validator