Theorem mp3an3an 1476

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  mp3an2ani  1477  unfilem2  9210  rankelun  9791  mul02  11319  fnn0ind  12623  supminf  12880  nn0p1elfzo  13652  faclbnd5  14255  pfxccatin12lem3  14689  mulre  15078  divalglem0  16357  algcvga  16543  infpn2  16879  prmgaplem7  17023  blssioo  24782  i1fsub  25697  itg1sub  25698  coesub  26244  dgrsub  26259  sincosq1eq  26498  logtayl2  26648  cxploglim  26963  uspgr2v1e2w  29342  ftc1anclem6  38080  plusmod5ne  47828  muldvdsfacgt  47863  io1ii  49425