Theorem mp3an2i 1376

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  mapen  7027  mapxpen  7029  en2eleq  7396  nnledivrp  9991  xsubge0  10106  iccen  10231  fldiv4lem1div2uz2  10556  frec2uzsucd  10653  seqp1g  10718  fnpfx  11248  cats1fvn  11335  seq3shft  11389  geolim2  12063  geoisum1c  12071  ntrivcvgap  12099  eflegeo  12252  sin01gt0  12313  cos01gt0  12314  3dvds  12415  gcdn0gt0  12539  uzwodc  12598  divgcdodd  12705  sqpweven  12737  2sqpwodd  12738  pythagtriplem4  12831  pythagtriplem11  12837  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pcfac  12913  4sqlemffi  12959  omctfn  13054  ssnnctlemct  13057  topnvalg  13324  imasmulr  13382  imasaddfnlemg  13387  gsumsplit1r  13471  gsumprval  13472  ismhm  13534  mhmex  13535  gsumfzz  13568  prdsinvlem  13681  scaffng  14313  lss1d  14387  zringinvg  14608  psrplusgg  14682  restbasg  14882  restco  14888  lmfval  14907  cnfval  14908  cnpval  14912  upxp  14986  uptx  14988  txrest  14990  xblm  15131  bdmet  15216  bdmopn  15218  reopnap  15260  cnopnap  15325  maxcncf  15329  mincncf  15330  dvidlemap  15405  dvcj  15423  plyval  15446  plysub  15467  eflt  15489  logdivlti  15595  perfectlem1  15713  perfectlem2  15714  gausslemma2dlem0i  15776  gausslemma2dlem4  15783  lgsquad2lem1  15800  lgsquad2lem2  15801  clwwlknon  16224  trilpolemisumle  16578