Theorem mp3an2i 1342

Description: mp3an 1337 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 1324	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	1, 2, 5	syl2anc 411	1 ⊢ (𝜓 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  mapen  6841  mapxpen  6843  en2eleq  7189  nnledivrp  9760  xsubge0  9875  iccen  10000  frec2uzsucd  10394  seq3shft  10838  geolim2  11511  geoisum1c  11519  ntrivcvgap  11547  eflegeo  11700  sin01gt0  11760  cos01gt0  11761  gcdn0gt0  11969  uzwodc  12028  divgcdodd  12133  sqpweven  12165  2sqpwodd  12166  pythagtriplem4  12258  pythagtriplem11  12264  pythagtriplem12  12265  pythagtriplem13  12266  pythagtriplem14  12267  pcfac  12338  omctfn  12434  ssnnctlemct  12437  topnvalg  12686  ismhm  12781  restbasg  13450  restco  13456  lmfval  13474  cnfval  13476  cnpval  13480  upxp  13554  uptx  13556  txrest  13558  xblm  13699  bdmet  13784  bdmopn  13786  reopnap  13820  cnopnap  13876  dvidlemap  13942  dvcj  13955  eflt  13978  logdivlti  14084  trilpolemisumle  14557