Theorem mp3an2i 1331

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

Syntax hints:   → wi 4   ∧ w3a 967

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 969

This theorem is referenced by:  mapen  6803  mapxpen  6805  en2eleq  7142  nnledivrp  9693  xsubge0  9808  iccen  9933  frec2uzsucd  10326  seq3shft  10766  geolim2  11439  geoisum1c  11447  ntrivcvgap  11475  eflegeo  11628  sin01gt0  11688  cos01gt0  11689  gcdn0gt0  11896  divgcdodd  12052  sqpweven  12084  2sqpwodd  12085  pythagtriplem4  12177  pythagtriplem11  12183  pythagtriplem12  12184  pythagtriplem13  12185  pythagtriplem14  12186  pcfac  12257  omctfn  12313  ssnnctlemct  12316  ressid  12392  topnvalg  12504  restbasg  12709  restco  12715  lmfval  12733  cnfval  12735  cnpval  12739  upxp  12813  uptx  12815  txrest  12817  xblm  12958  bdmet  13043  bdmopn  13045  reopnap  13079  cnopnap  13135  dvidlemap  13201  dvcj  13214  eflt  13237  logdivlti  13343  trilpolemisumle  13751