Theorem mp3an3an 1496

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an2ani  1497  unfilem2  9279  rankelun  9857  mul02  11415  fnn0ind  12723  supminf  12987  nn0p1elfzo  13760  faclbnd5  14364  pfxccatin12lem3  14803  mulre  15210  divalglem0  16487  algcvga  16673  infpn2  17009  prmgaplem7  17153  blssioo  25022  i1fsub  25937  itg1sub  25938  coesub  26484  dgrsub  26499  sincosq1eq  26747  logtayl2  26897  cxploglim  27212  uspgr2v1e2w  29697  ftc1anclem6  38434  findcard4  38450  fourierdlem48  46969  plusmod5ne  48226  muldvdsfacgt  48261  io1ii  49834