Theorem mp3an2i 1337

Description: mp3an 1332 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an2i.1	⊢ 𝜑
mp3an2i.2	⊢ (𝜓 → 𝜒)
mp3an2i.3	⊢ (𝜓 → 𝜃)
mp3an2i.4	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
mp3an2i	⊢ (𝜓 → 𝜏)

Proof of Theorem mp3an2i

Step	Hyp	Ref	Expression
1		mp3an2i.2	. 2 ⊢ (𝜓 → 𝜒)
2		mp3an2i.3	. 2 ⊢ (𝜓 → 𝜃)
3		mp3an2i.1	. . 3 ⊢ 𝜑
4		mp3an2i.4	. . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
5	3, 4	mp3an1 1319	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	1, 2, 5	syl2anc 409	1 ⊢ (𝜓 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  mapen  6824  mapxpen  6826  en2eleq  7172  nnledivrp  9723  xsubge0  9838  iccen  9963  frec2uzsucd  10357  seq3shft  10802  geolim2  11475  geoisum1c  11483  ntrivcvgap  11511  eflegeo  11664  sin01gt0  11724  cos01gt0  11725  gcdn0gt0  11933  uzwodc  11992  divgcdodd  12097  sqpweven  12129  2sqpwodd  12130  pythagtriplem4  12222  pythagtriplem11  12228  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem14  12231  pcfac  12302  omctfn  12398  ssnnctlemct  12401  ressid  12479  topnvalg  12591  ismhm  12685  restbasg  12962  restco  12968  lmfval  12986  cnfval  12988  cnpval  12992  upxp  13066  uptx  13068  txrest  13070  xblm  13211  bdmet  13296  bdmopn  13298  reopnap  13332  cnopnap  13388  dvidlemap  13454  dvcj  13467  eflt  13490  logdivlti  13596  trilpolemisumle  14070