Theorem mp3an3an 1463

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  mp3an2ani  1464  unfilem2  8785  rankelun  9303  mul02  10820  fnn0ind  12084  supminf  12338  nn0p1elfzo  13083  faclbnd5  13661  pfxccatin12lem3  14096  mulre  14482  divalglem0  15746  algcvga  15925  infpn2  16251  prmgaplem7  16395  blssioo  23405  i1fsub  24311  itg1sub  24312  coesub  24849  dgrsub  24864  sincosq1eq  25100  logtayl2  25247  cxploglim  25557  uspgr2v1e2w  27035  ftc1anclem6  34974