Theorem mp3an2ani 1470

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  01sqrexlem4  15168  coprm  16638  frlmssuvc1  21749  en2top  22929  tgrest  23103  pi1cof  25015  voliunlem1  25507  dvnfre  25912  dvcnvre  25980  ig1pdvds  26141  taylthlem2  26338  taylthlem2OLD  26339  chtub  27179  2lgsoddprmlem2  27376  fzo0opth  32883  nsgmgc  33493  omabs2  43574  isosctrlem1ALT  45174  chnsubseqwl  47123  odz2prm2pw  47809  lighneallem4  47856  itcovalpclem2  48917  itcovalt2lem2  48922