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

Theorem 3imp21 1113
Description: The importation inference 3imp 1110 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 1122 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 1112 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1086
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 1088
This theorem is referenced by:  3com12  1122  sotri3  6153  isinf  9294  isinfOLD  9295  infssuni  9384  fin1a2lem10  10447  elfz1b  13630  bernneq  14265  expnngt1  14277  swrdco  14873  dfgcd2  16580  lmodvsmmulgdi  20912  mamufacex  22416  gausslemma2dlem1a  27424  ssltun1  27868  ssltright  27925  expsgt0  28430  upgrewlkle2  29639  pthdivtx  29762  clwwlkinwwlk  30069  upgr3v3e3cycl  30209  upgr4cycl4dv4e  30214  numclwwlk2lem1lem  30371  frgrregord013  30424  ax6e2ndeqALT  44929  fmtnofac2  47494
  Copyright terms: Public domain W3C validator