Theorem mp3an2ani 1477

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  01sqrexlem4  15202  coprm  16676  frlmssuvc1  21773  en2top  22972  tgrest  23146  pi1cof  25048  voliunlem1  25539  dvnfre  25941  dvcnvre  26008  ig1pdvds  26167  taylthlem2  26361  chtub  27197  2lgsoddprmlem2  27394  fzo0opth  32899  nsgmgc  33499  omabs2  43792  isosctrlem1ALT  45392  chnsubseqwl  47338  odz2prm2pw  48055  lighneallem4  48102  itcovalpclem2  49176  itcovalt2lem2  49181