Theorem mp3an2ani 1464

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

Step	Hyp	Ref	Expression
1		mp3an2ani.1	. . 3 ⊢ 𝜑
2		mp3an2ani.2	. . 3 ⊢ (𝜓 → 𝜒)
3		mp3an2ani.3	. . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
4		mp3an2ani.4	. . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
5	1, 2, 3, 4	mp3an3an 1463	. 2 ⊢ ((𝜓 ∧ (𝜓 ∧ 𝜃)) → 𝜂)
6	5	anabss5 666	1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  01sqrexlem4  15228  coprm  16685  frlmssuvc1  21745  en2top  22932  tgrest  23107  pi1cof  25030  voliunlem1  25523  dvnfre  25928  dvcnvre  25996  ig1pdvds  26159  taylthlem2  26354  taylthlem2OLD  26355  chtub  27190  2lgsoddprmlem2  27387  fzo0opth  32655  nsgmgc  33224  omabs2  42900  isosctrlem1ALT  44512  odz2prm2pw  47037  lighneallem4  47084  itcovalpclem2  47927  itcovalt2lem2  47932