Theorem mp3an3an 1493

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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

This theorem is referenced by:  mp3an2ani  1494  unfilem2  9266  rankelun  9844  mul02  11388  fnn0ind  12695  supminf  12959  nn0p1elfzo  13731  faclbnd5  14334  pfxccatin12lem3  14769  mulre  15172  divalglem0  16451  algcvga  16637  infpn2  16973  prmgaplem7  17117  blssioo  24921  i1fsub  25836  itg1sub  25837  coesub  26383  dgrsub  26398  sincosq1eq  26643  logtayl2  26793  cxploglim  27108  uspgr2v1e2w  29542  ftc1anclem6  38272  fourierdlem48  46795  plusmod5ne  48012  muldvdsfacgt  48047  io1ii  49619