Theorem mp3an2i 1383

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  mapsnend  7089  mapen  7136  mapxpen  7138  mapunen  7141  en2eleq  7537  nnledivrp  10146  xsubge0  10262  iccen  10388  fzen  10426  fldiv4lem1div2uz2  10719  frec2uzsucd  10816  seqp1g  10881  fnpfx  11427  cats1fvn  11514  seq3shft  11581  geolim2  12257  geoisum1c  12265  ntrivcvgap  12293  eflegeo  12446  sin01gt0  12507  cos01gt0  12508  3dvds  12609  gcdn0gt0  12733  uzwodc  12792  divgcdodd  12899  sqpweven  12931  2sqpwodd  12932  pythagtriplem4  13025  pythagtriplem11  13031  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pcfac  13107  4sqlemffi  13153  ballotfilemfcc  13211  ballotfilemfmpn  13212  omctfn  13312  ssnnctlemct  13315  topnvalg  13582  imasmulr  13607  imasaddfnlemg  13612  gzsumsplit1r  13692  ismhm  13745  mhmex  13746  gsumvalfi  14129  prdsinvlem  14173  scaffng  14618  lss1d  14692  zringinvg  14911  psrplusgg  14992  restbasg  15192  restco  15198  lmfval  15217  cnfval  15218  cnpval  15222  upxp  15296  uptx  15298  txrest  15300  xblm  15441  bdmet  15526  bdmopn  15528  reopnap  15570  cnopnap  15635  maxcncf  15639  mincncf  15640  dvidlemap  15715  dvcj  15733  plyval  15756  plysub  15777  eflt  15799  logdivlti  15905  perfectlem1  16027  perfectlem2  16028  gausslemma2dlem0i  16090  gausslemma2dlem4  16097  lgsquad2lem1  16114  lgsquad2lem2  16115  clwwlknon  16584  trilpolemisumle  16992