Theorem mp3an2ani 1491

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  01sqrexlem4  15274  coprm  16748  frlmssuvc1  21848  en2top  23047  tgrest  23221  pi1cof  25123  voliunlem1  25614  dvnfre  26016  dvcnvre  26083  ig1pdvds  26242  taylthlem2  26439  chtub  27278  2lgsoddprmlem2  27475  fzo0opth  33007  nsgmgc  33600  omabs2  43914  isosctrlem1ALT  45514  chnsubseqwl  47460  odz2prm2pw  48177  lighneallem4  48224  itcovalpclem2  49298  itcovalt2lem2  49303