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

Theorem 3imp21 1110
 Description: The importation inference 3imp 1107 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 1119 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 1109 1 ((𝜓𝜑𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1083 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 209  df-an 399  df-3an 1085 This theorem is referenced by:  3com12  1119  sotri3  5993  isinf  8734  infssuni  8818  fin1a2lem10  9834  elfz1b  12979  bernneq  13593  expnngt1  13605  swrdco  14202  dfgcd2  15897  lmodvsmmulgdi  19672  mamufacex  21003  gausslemma2dlem1a  25944  upgrewlkle2  27391  pthdivtx  27513  clwwlkinwwlk  27821  upgr3v3e3cycl  27962  upgr4cycl4dv4e  27967  numclwwlk2lem1lem  28124  frgrregord013  28177  ax6e2ndeqALT  41271  fmtnofac2  43738
 Copyright terms: Public domain W3C validator