Theorem mp3an3an 1469

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mp3an2ani  1470  unfilem2  9232  rankelun  9804  mul02  11331  fnn0ind  12612  supminf  12873  nn0p1elfzo  13642  faclbnd5  14242  pfxccatin12lem3  14675  mulre  15065  divalglem0  16341  algcvga  16527  infpn2  16862  prmgaplem7  17006  blssioo  24718  i1fsub  25644  itg1sub  25645  coesub  26197  dgrsub  26213  sincosq1eq  26456  logtayl2  26606  cxploglim  26923  uspgr2v1e2w  29233  ftc1anclem6  37687  plusmod5ne  47341  io1ii  48904