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  6836  mapxpen  6838  en2eleq  7184  nnledivrp  9735  xsubge0  9850  iccen  9975  frec2uzsucd  10369  seq3shft  10813  geolim2  11486  geoisum1c  11494  ntrivcvgap  11522  eflegeo  11675  sin01gt0  11735  cos01gt0  11736  gcdn0gt0  11944  uzwodc  12003  divgcdodd  12108  sqpweven  12140  2sqpwodd  12141  pythagtriplem4  12233  pythagtriplem11  12239  pythagtriplem12  12240  pythagtriplem13  12241  pythagtriplem14  12242  pcfac  12313  omctfn  12409  ssnnctlemct  12412  ressid  12490  topnvalg  12620  ismhm  12714  restbasg  13237  restco  13243  lmfval  13261  cnfval  13263  cnpval  13267  upxp  13341  uptx  13343  txrest  13345  xblm  13486  bdmet  13571  bdmopn  13573  reopnap  13607  cnopnap  13663  dvidlemap  13729  dvcj  13742  eflt  13765  logdivlti  13871  trilpolemisumle  14345