Theorem mp3an2ani 1498

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 1497	. 2 ⊢ ((𝜓 ∧ (𝜓 ∧ 𝜃)) → 𝜂)
6	5	anabss5 681	1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  01sqrexlem4  15438  coprm  16913  frlmssuvc1  22127  en2top  23330  tgrest  23504  pi1cof  25407  voliunlem1  25898  dvnfre  26299  dvcnvre  26366  ig1pdvds  26525  taylthlem2  26728  chtub  27566  2lgsoddprmlem2  27763  fzo0opth  33462  nsgmgc  34030  omabs2  44524  isosctrlem1ALT  46105  chnsubseqwl  48092  odz2prm2pw  48851  lighneallem4  48898  itcovalpclem2  49986  itcovalt2lem2  49991