Theorem mp3an2i 1288

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

Syntax hints:   → wi 4   ∧ w3a 930

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

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

This theorem is referenced by:  mapen  6669  mapxpen  6671  ctssdclemr  6911  en2eleq  6960  nnledivrp  9394  xsubge0  9505  frec2uzsucd  10015  seq3shft  10451  geolim2  11120  geoisum1c  11128  eflegeo  11206  sin01gt0  11266  cos01gt0  11267  gcdn0gt0  11461  divgcdodd  11614  sqpweven  11645  2sqpwodd  11646  ressid  11802  topnvalg  11914  restbasg  12119  restco  12125  lmfval  12143  cnfval  12145  cnpval  12148  upxp  12222  uptx  12224  txrest  12226  xblm  12345  bdmet  12430  bdmopn  12432  dvidlemap  12533  trilpolemisumle  12815