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

Theorem 3imp21 1116
Description: The importation inference 3imp 1113 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 1125 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 1115 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1089
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 210  df-an 400  df-3an 1091
This theorem is referenced by:  3com12  1125  sotri3  6009  isinf  8915  infssuni  8991  fin1a2lem10  10047  elfz1b  13205  bernneq  13820  expnngt1  13832  swrdco  14426  dfgcd2  16130  lmodvsmmulgdi  19958  mamufacex  21312  gausslemma2dlem1a  26270  upgrewlkle2  27718  pthdivtx  27840  clwwlkinwwlk  28147  upgr3v3e3cycl  28287  upgr4cycl4dv4e  28292  numclwwlk2lem1lem  28449  frgrregord013  28502  ssltun1  33765  ssltright  33818  ax6e2ndeqALT  42252  fmtnofac2  44722
  Copyright terms: Public domain W3C validator