Metamath Proof Explorer


Theorem mp3an2ani

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

Ref Expression
Hypotheses mp3an2ani.1 φ
mp3an2ani.2 ψχ
mp3an2ani.3 ψθτ
mp3an2ani.4 φχτη
Assertion mp3an2ani ψθη

Proof

Step Hyp Ref Expression
1 mp3an2ani.1 φ
2 mp3an2ani.2 ψχ
3 mp3an2ani.3 ψθτ
4 mp3an2ani.4 φχτη
5 1 2 3 4 mp3an3an ψψθη
6 5 anabss5 ψθη