Theorem mp3an2i 1462

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

Syntax hints:   → wi 4   ∧ w3a 1083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  wfrlem17  7974  onnseq  7984  oeoalem  8225  oeoelem  8227  domssex2  8680  domssex  8681  sniffsupp  8876  cantnfp1lem1  9144  en2eleq  9437  en2other2  9438  infxpenc  9447  infxpenc2lem1  9448  mappwen  9541  dfac12lem2  9573  ackbij1b  9664  fin23lem26  9750  ttukeylem5  9938  gchac  10106  wunex2  10163  00id  10818  fiminreOLD  11593  nngt1ne1  11669  gtndiv  12062  nn01to3  12344  rpnnen1lem2  12379  nnledivrp  12504  xrre3  12567  max0sub  12592  xsubge0  12657  xrub  12708  bernneq  13593  faclbnd6  13662  bc0k  13674  wrdlen2i  14307  sqrlem5  14609  sqrlem7  14611  sqreulem  14722  0.999...  15240  bpoly3  15415  fsumcube  15417  cos2t  15534  cos2tsin  15535  sin01gt0  15546  cos01gt0  15547  absefib  15554  efieq1re  15555  3dvds  15683  nno  15736  gcdcllem3  15853  gcdn0gt0  15869  divgcdodd  16057  pythagtriplem4  16159  pythagtriplem11  16165  pythagtriplem12  16166  pythagtriplem13  16167  pythagtriplem14  16168  pcfac  16238  prmreclem1  16255  vdwlem12  16331  ramval  16347  ramub2  16353  prmolelcmf  16387  prmgaplcmlem2  16391  firest  16709  yonffthlem  17535  gsumval2a  17898  prdsinvlem  18211  f1otrspeq  18578  pmtrf  18586  pmtrmvd  18587  pmtrfinv  18592  gexex  18976  cnaddinv  18994  prdsmgp  19363  opsrtoslem2  20268  evls1val  20486  evls1sca  20489  zringlpirlem1  20634  zringinvg  20637  frgpcyg  20723  redvr  20764  frlmphllem  20927  frlmup4  20948  smadiadetlem1  21274  smadiadetlem3lem0  21277  smadiadet  21282  d0mat2pmat  21349  chpmat0d  21445  neiptoptop  21742  upxp  22234  uptx  22236  pt1hmeo  22417  tgpconncompeqg  22723  qustgplem  22732  cnextucn  22915  psmetge0  22925  xmetge0  22957  xbln0  23027  tmsxpsval2  23152  metustid  23167  icopnfcld  23379  iocmnfcld  23380  ioo2blex  23405  tgioo  23407  blcvx  23409  xrsmopn  23423  recld2  23425  metdcn2  23450  cnmptre  23534  icchmeo  23548  cnheiborlem  23561  cnheibor  23562  lebnumii  23573  phtpyco2  23597  pi1xfrf  23660  pi1xfr  23662  pi1xfrcnvlem  23663  pi1xfrcnv  23664  pi1coghm  23668  ehleudisval  24025  ovolmge0  24081  ovolctb2  24096  nulmbl2  24140  unmbl  24141  ioombl1lem4  24165  ovolioo  24172  uniioombllem2  24187  uniioombllem4  24190  uniioombllem5  24191  uniioombllem6  24192  opnmbllem  24205  volcn  24210  i1fadd  24299  itg1addlem2  24301  i1fres  24309  itgle  24413  itgsplitioo  24441  ellimc3  24480  limcflflem  24481  limcflf  24482  limcmo  24483  limcres  24487  limciun  24495  perfdvf  24504  dvidlem  24516  dvnres  24531  dvlipcn  24594  dv11cn  24601  lhop2  24615  dvcnvrelem2  24618  plysub  24812  coeeulem  24817  plydiveu  24890  vieta1lem2  24903  plyexmo  24905  aaliou2b  24933  taylfval  24950  psercn  25017  pserdvlem2  25019  pserdv  25020  logdivlti  25206  efopnlem2  25243  acoscos  25474  xrlimcnp  25549  efrlim  25550  lgamucov  25618  basellem9  25669  perfectlem1  25808  perfectlem2  25809  lgsqrlem4  25928  gausslemma2dlem4  25948  lgsquad2lem1  25963  lgsquad2lem2  25964  dchrisum0lem1  26095  pntlem3  26188  pntleml  26190  qrngdiv  26203  ttgcontlem1  26674  brbtwn2  26694  colinearalglem4  26698  ax5seglem1  26717  axcontlem4  26756  axcontlem7  26759  wlkp1lem3  27460  wlkp1lem7  27464  wlkp1lem8  27465  pthdlem1  27550  conngrv2edg  27977  txomap  31102  revpfxsfxrev  32366  cvmlift2lem10  32563  nosupbday  33209  itg2gt0cn  34951  enrelmap  40349  k0004lem3  40505  sineq0ALT  41277  xlimconst  42112  odz2prm2pw  43732  fmtno4prmfac  43741  lighneallem3  43779  lighneallem4a  43780  lighneallem4  43782  fllog2  44635  prelrrx2b  44708  rrxsphere  44742  2sphere  44743  line2  44746  line2x  44748  line2y  44749