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

Theorem mp3an2ani 1470
Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
Hypotheses
Ref Expression
mp3an2ani.1 𝜑
mp3an2ani.2 (𝜓𝜒)
mp3an2ani.3 ((𝜓𝜃) → 𝜏)
mp3an2ani.4 ((𝜑𝜒𝜏) → 𝜂)
Assertion
Ref Expression
mp3an2ani ((𝜓𝜃) → 𝜂)

Proof of Theorem mp3an2ani
StepHypRef Expression
1 mp3an2ani.1 . . 3 𝜑
2 mp3an2ani.2 . . 3 (𝜓𝜒)
3 mp3an2ani.3 . . 3 ((𝜓𝜃) → 𝜏)
4 mp3an2ani.4 . . 3 ((𝜑𝜒𝜏) → 𝜂)
51, 2, 3, 4mp3an3an 1469 . 2 ((𝜓 ∧ (𝜓𝜃)) → 𝜂)
65anabss5 668 1 ((𝜓𝜃) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 1089
This theorem is referenced by:  01sqrexlem4  15284  coprm  16748  frlmssuvc1  21814  en2top  22992  tgrest  23167  pi1cof  25092  voliunlem1  25585  dvnfre  25990  dvcnvre  26058  ig1pdvds  26219  taylthlem2  26416  taylthlem2OLD  26417  chtub  27256  2lgsoddprmlem2  27453  fzo0opth  32807  nsgmgc  33440  omabs2  43345  isosctrlem1ALT  44954  odz2prm2pw  47550  lighneallem4  47597  itcovalpclem2  48592  itcovalt2lem2  48597
  Copyright terms: Public domain W3C validator