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

Theorem mp3an2ani 1467
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 1466 . 2 ((𝜓 ∧ (𝜓𝜃)) → 𝜂)
65anabss5 668 1 ((𝜓𝜃) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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:  01sqrexlem4  15281  coprm  16745  frlmssuvc1  21832  en2top  23008  tgrest  23183  pi1cof  25106  voliunlem1  25599  dvnfre  26005  dvcnvre  26073  ig1pdvds  26234  taylthlem2  26431  taylthlem2OLD  26432  chtub  27271  2lgsoddprmlem2  27468  fzo0opth  32813  nsgmgc  33420  omabs2  43322  isosctrlem1ALT  44932  odz2prm2pw  47488  lighneallem4  47535  itcovalpclem2  48521  itcovalt2lem2  48526
  Copyright terms: Public domain W3C validator