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

Theorem mp3an2ani 1459
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 1458 . 2 ((𝜓 ∧ (𝜓𝜃)) → 𝜂)
65anabss5 664 1 ((𝜓𝜃) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  sqrlem4  14593  gcdmultipleOLD  15888  coprm  16043  frlmssuvc1  20866  en2top  21521  tgrest  21695  pi1cof  23590  voliunlem1  24078  dvnfre  24476  dvcnvre  24543  ig1pdvds  24697  taylthlem2  24889  chtub  25715  2lgsoddprmlem2  25912  isosctrlem1ALT  41145  odz2prm2pw  43602  lighneallem4  43652
  Copyright terms: Public domain W3C validator