Metamath Proof Explorer

Theorem mp3an3an

Description: mp3an with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016)

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


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