Theorem mp3an2i 1468

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  onnseq  8313  oeoalem  8560  oeoelem  8562  domssex2  9101  domssex  9102  dif1enOLD  9126  sniffsupp  9351  cantnfp1lem1  9631  en2eleq  9961  en2other2  9962  infxpenc  9971  infxpenc2lem1  9972  mappwen  10065  dfac12lem2  10098  ackbij1b  10191  fin23lem26  10278  ttukeylem5  10466  gchac  10634  wunex2  10691  00id  11349  nngt1ne1  12215  gtndiv  12611  nn01to3  12900  rpnnen1lem2  12936  nnledivrp  13065  xrre3  13131  max0sub  13156  xsubge0  13221  xrub  13272  bernneq  14194  faclbnd6  14264  bc0k  14276  brfi1indALT  14475  wrdlen2i  14908  01sqrexlem5  15212  01sqrexlem7  15214  sqreulem  15326  0.999...  15847  bpoly3  16024  fsumcube  16026  cos2t  16146  cos2tsin  16147  sin01gt0  16158  cos01gt0  16159  absefib  16166  efieq1re  16167  3dvds  16301  nno  16352  gcdcllem3  16471  gcdn0gt0  16488  divgcdodd  16680  pythagtriplem4  16790  pythagtriplem11  16796  pythagtriplem12  16797  pythagtriplem13  16798  pythagtriplem14  16799  pcfac  16870  prmreclem1  16887  vdwlem12  16963  ramval  16979  ramub2  16985  prmolelcmf  17019  prmgaplcmlem2  17023  firest  17395  yonffthlem  18243  gsumval2a  18612  prdsinvlem  18981  f1otrspeq  19377  pmtrf  19385  pmtrmvd  19386  pmtrfinv  19391  gexex  19783  cnaddinv  19801  prdsmgp  20060  zringlpirlem1  21372  zringinvg  21375  pzriprnglem10  21400  frgpcyg  21483  redvr  21526  frlmphllem  21689  frlmup4  21710  evls1val  22207  evls1sca  22210  smadiadetlem1  22549  smadiadetlem3lem0  22552  smadiadet  22557  d0mat2pmat  22625  chpmat0d  22721  neiptoptop  23018  upxp  23510  uptx  23512  pt1hmeo  23693  tgpconncompeqg  23999  qustgplem  24008  cnextucn  24190  psmetge0  24200  xmetge0  24232  xbln0  24302  tmsxpsval2  24427  metustid  24442  icopnfcld  24655  iocmnfcld  24656  ioo2blex  24682  tgioo  24684  blcvx  24686  xrsmopn  24701  recld2  24703  metdcn2  24728  cnmptre  24821  icchmeo  24838  icchmeoOLD  24839  cnheiborlem  24853  cnheibor  24854  lebnumii  24865  phtpyco2  24889  pi1xfrf  24953  pi1xfr  24955  pi1xfrcnvlem  24956  pi1xfrcnv  24957  pi1coghm  24961  ehleudisval  25319  ovolmge0  25378  ovolctb2  25393  nulmbl2  25437  unmbl  25438  ioombl1lem4  25462  ovolioo  25469  uniioombllem2  25484  uniioombllem4  25487  uniioombllem5  25488  uniioombllem6  25489  opnmbllem  25502  volcn  25507  i1fadd  25596  itg1addlem2  25598  i1fres  25606  itgle  25711  itgsplitioo  25739  ellimc3  25780  limcflflem  25781  limcflf  25782  limcmo  25783  limcres  25787  limciun  25795  perfdvf  25804  dvidlem  25816  dvnres  25833  dvlipcn  25899  dv11cn  25906  lhop2  25920  dvcnvrelem2  25923  tdeglem4  25965  plysub  26124  coeeulem  26129  plydiveu  26206  vieta1lem2  26219  plyexmo  26221  aaliou2b  26249  taylfval  26266  psercn  26336  pserdvlem2  26338  pserdv  26339  logdivlti  26529  efopnlem2  26566  acoscos  26803  xrlimcnp  26878  efrlim  26879  efrlimOLD  26880  lgamucov  26948  basellem9  26999  perfectlem1  27140  perfectlem2  27141  lgsqrlem4  27260  gausslemma2dlem4  27280  lgsquad2lem1  27295  lgsquad2lem2  27296  dchrisum0lem1  27427  pntlem3  27520  pntleml  27522  qrngdiv  27535  nosupbday  27617  noinfbday  27632  noetainflem4  27652  madebdaylemlrcut  27810  onsiso  28169  ttgcontlem1  28812  brbtwn2  28832  colinearalglem4  28836  ax5seglem1  28855  axcontlem4  28894  axcontlem7  28897  wlkp1lem3  29603  wlkp1lem7  29607  wlkp1lem8  29608  pthdlem1  29696  conngrv2edg  30124  mptiffisupp  32616  elringlsm  33364  txomap  33824  rmulccn  33918  revpfxsfxrev  35103  cvxpconn  35229  cvxsconn  35230  cvmlift2lem10  35299  knoppcnlem10  36490  itg2gt0cn  37669  resubeqsub  42418  flt4lem7  42647  nna4b4nsq  42648  omabs2  43321  nadd2rabex  43375  enrelmap  43986  k0004lem3  44138  sineq0ALT  44926  xlimconst  45823  2ltceilhalf  47329  odz2prm2pw  47564  fmtno4prmfac  47573  lighneallem3  47608  lighneallem4a  47609  lighneallem4  47611  gpg3kgrtriexlem3  48076  fllog2  48557  2arymptfv  48639  prelrrx2b  48703  rrxsphere  48737  2sphere  48738  line2  48741  line2x  48743  line2y  48744