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  7015  mapxpen  7017  en2eleq  7384  nnledivrp  9974  xsubge0  10089  iccen  10214  fldiv4lem1div2uz2  10538  frec2uzsucd  10635  seqp1g  10700  fnpfx  11225  cats1fvn  11312  seq3shft  11365  geolim2  12039  geoisum1c  12047  ntrivcvgap  12075  eflegeo  12228  sin01gt0  12289  cos01gt0  12290  3dvds  12391  gcdn0gt0  12515  uzwodc  12574  divgcdodd  12681  sqpweven  12713  2sqpwodd  12714  pythagtriplem4  12807  pythagtriplem11  12813  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem14  12816  pcfac  12889  4sqlemffi  12935  omctfn  13030  ssnnctlemct  13033  topnvalg  13300  imasmulr  13358  imasaddfnlemg  13363  gsumsplit1r  13447  gsumprval  13448  ismhm  13510  mhmex  13511  gsumfzz  13544  prdsinvlem  13657  scaffng  14289  lss1d  14363  zringinvg  14584  psrplusgg  14658  restbasg  14858  restco  14864  lmfval  14883  cnfval  14884  cnpval  14888  upxp  14962  uptx  14964  txrest  14966  xblm  15107  bdmet  15192  bdmopn  15194  reopnap  15236  cnopnap  15301  maxcncf  15305  mincncf  15306  dvidlemap  15381  dvcj  15399  plyval  15422  plysub  15443  eflt  15465  logdivlti  15571  perfectlem1  15689  perfectlem2  15690  gausslemma2dlem0i  15752  gausslemma2dlem4  15759  lgsquad2lem1  15776  lgsquad2lem2  15777  trilpolemisumle  16494