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  9255  rankelun  9825  mul02  11352  fnn0ind  12633  supminf  12894  nn0p1elfzo  13663  faclbnd5  14263  pfxccatin12lem3  14697  mulre  15087  divalglem0  16363  algcvga  16549  infpn2  16884  prmgaplem7  17028  blssioo  24683  i1fsub  25609  itg1sub  25610  coesub  26162  dgrsub  26178  sincosq1eq  26421  logtayl2  26571  cxploglim  26888  uspgr2v1e2w  29178  ftc1anclem6  37692  plusmod5ne  47346  io1ii  48909