Theorem mp3an3an 1496

Description: mp3an 1490 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an3an.1	⊢ 𝜑
mp3an3an.2	⊢ (𝜓 → 𝜒)
mp3an3an.3	⊢ (𝜃 → 𝜏)
mp3an3an.4	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
mp3an3an	⊢ ((𝜓 ∧ 𝜃) → 𝜂)

Proof of Theorem mp3an3an

Step	Hyp	Ref	Expression
1		mp3an3an.2	. 2 ⊢ (𝜓 → 𝜒)
2		mp3an3an.3	. 2 ⊢ (𝜃 → 𝜏)
3		mp3an3an.1	. . 3 ⊢ 𝜑
4		mp3an3an.4	. . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)
5	3, 4	mp3an1 1477	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜂)
6	1, 2, 5	syl2an 608	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:  mp3an2ani  1497  unfilem2  9276  rankelun  9858  mul02  11445  fnn0ind  12753  supminf  13017  nn0p1elfzo  13791  faclbnd5  14395  pfxccatin12lem3  14834  mulre  15241  divalglem0  16516  algcvga  16702  infpn2  17038  prmgaplem7  17182  blssioo  25061  i1fsub  25976  itg1sub  25977  coesub  26523  dgrsub  26538  sincosq1eq  26790  logtayl2  26939  cxploglim  27254  uspgr2v1e2w  29751  ftc1anclem6  38530  findcard4  38546  fourierdlem48  47080  plusmod5ne  48337  muldvdsfacgt  48372  io1ii  49945