Theorem mp3an2i 1332

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

Syntax hints:   → wi 4   ∧ w3a 968

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 970

This theorem is referenced by:  mapen  6812  mapxpen  6814  en2eleq  7151  nnledivrp  9702  xsubge0  9817  iccen  9942  frec2uzsucd  10336  seq3shft  10780  geolim2  11453  geoisum1c  11461  ntrivcvgap  11489  eflegeo  11642  sin01gt0  11702  cos01gt0  11703  gcdn0gt0  11911  uzwodc  11970  divgcdodd  12075  sqpweven  12107  2sqpwodd  12108  pythagtriplem4  12200  pythagtriplem11  12206  pythagtriplem12  12207  pythagtriplem13  12208  pythagtriplem14  12209  pcfac  12280  omctfn  12376  ssnnctlemct  12379  ressid  12456  topnvalg  12568  restbasg  12808  restco  12814  lmfval  12832  cnfval  12834  cnpval  12838  upxp  12912  uptx  12914  txrest  12916  xblm  13057  bdmet  13142  bdmopn  13144  reopnap  13178  cnopnap  13234  dvidlemap  13300  dvcj  13313  eflt  13336  logdivlti  13442  trilpolemisumle  13917