Theorem mp3an3an 1495

Description: mp3an 1489 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 1476	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜂)
6	1, 2, 5	syl2an 607	1 ⊢ ((𝜓 ∧ 𝜃) → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  mp3an2ani  1496  unfilem2  9264  rankelun  9842  mul02  11394  fnn0ind  12701  supminf  12965  nn0p1elfzo  13738  faclbnd5  14341  pfxccatin12lem3  14776  mulre  15179  divalglem0  16457  algcvga  16643  infpn2  16979  prmgaplem7  17123  blssioo  24963  i1fsub  25878  itg1sub  25879  coesub  26425  dgrsub  26440  sincosq1eq  26688  logtayl2  26838  cxploglim  27153  uspgr2v1e2w  29612  ftc1anclem6  38377  fourierdlem48  46896  plusmod5ne  48116  muldvdsfacgt  48151  io1ii  49727