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

Theorem imim12 105
Description: Closed form of imim12i 62 and of 3syl 18. (Contributed by BJ, 16-Jul-2019.)
Assertion
Ref Expression
imim12 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜓𝜒) → (𝜑𝜃))))

Proof of Theorem imim12
StepHypRef Expression
1 imim2 58 . 2 ((𝜒𝜃) → ((𝜓𝜒) → (𝜓𝜃)))
2 imim1 83 . 2 ((𝜑𝜓) → ((𝜓𝜃) → (𝜑𝜃)))
31, 2syl9r 78 1 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜓𝜒) → (𝜑𝜃))))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  bj-nnfim1  33970  bj-nnfim2  33971
  Copyright terms: Public domain W3C validator