Theorem mp3an3an 1497

Description: mp3an 1491 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 1478	. 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  1498  unfilem2  9323  rankelun  9913  mul02  11512  fnn0ind  12822  supminf  13086  nn0p1elfzo  13861  faclbnd5  14466  pfxccatin12lem3  14906  mulre  15314  divalglem0  16589  algcvga  16780  infpn2  17117  prmgaplem7  17261  blssioo  25141  i1fsub  26056  itg1sub  26057  coesub  26603  dgrsub  26618  sincosq1eq  26868  logtayl2  27017  cxploglim  27332  uspgr2v1e2w  29859  ftc1anclem6  38807  findcard4  38823  fourierdlem48  47367  plusmod5ne  48624  muldvdsfacgt  48659  io1ii  50238