Theorem mp3an3an 1490

Description: mp3an 1484 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 1471	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜂)
6	1, 2, 5	syl2an 605	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:  mp3an2ani  1491  unfilem2  9252  rankelun  9832  mul02  11363  fnn0ind  12674  supminf  12938  nn0p1elfzo  13710  faclbnd5  14313  pfxccatin12lem3  14747  mulre  15150  divalglem0  16429  algcvga  16615  infpn2  16951  prmgaplem7  17095  blssioo  24857  i1fsub  25772  itg1sub  25773  coesub  26319  dgrsub  26334  sincosq1eq  26579  logtayl2  26729  cxploglim  27044  uspgr2v1e2w  29454  ftc1anclem6  38202  fourierdlem48  46733  plusmod5ne  47950  muldvdsfacgt  47985  io1ii  49547