Theorem mp3an2i 1469

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  onnseq  8288  oeoalem  8536  oeoelem  8538  domssex2  9079  domssex  9080  sniffsupp  9317  cantnfp1lem1  9601  en2eleq  9932  en2other2  9933  infxpenc  9942  infxpenc2lem1  9943  mappwen  10036  dfac12lem2  10069  ackbij1b  10162  fin23lem26  10249  ttukeylem5  10437  gchac  10606  wunex2  10663  00id  11322  nngt1ne1  12188  gtndiv  12583  nn01to3  12868  rpnnen1lem2  12904  nnledivrp  13033  xrre3  13100  max0sub  13125  xsubge0  13190  xrub  13241  bernneq  14166  faclbnd6  14236  bc0k  14248  brfi1indALT  14447  wrdlen2i  14879  01sqrexlem5  15183  01sqrexlem7  15185  sqreulem  15297  0.999...  15818  bpoly3  15995  fsumcube  15997  cos2t  16117  cos2tsin  16118  sin01gt0  16129  cos01gt0  16130  absefib  16137  efieq1re  16138  3dvds  16272  nno  16323  gcdcllem3  16442  gcdn0gt0  16459  divgcdodd  16651  pythagtriplem4  16761  pythagtriplem11  16767  pythagtriplem12  16768  pythagtriplem13  16769  pythagtriplem14  16770  pcfac  16841  prmreclem1  16858  vdwlem12  16934  ramval  16950  ramub2  16956  prmolelcmf  16990  prmgaplcmlem2  16994  firest  17366  yonffthlem  18219  gsumval2a  18624  prdsinvlem  18996  f1otrspeq  19393  pmtrf  19401  pmtrmvd  19402  pmtrfinv  19407  gexex  19799  cnaddinv  19817  prdsmgp  20103  zringlpirlem1  21434  zringinvg  21437  pzriprnglem10  21462  frgpcyg  21545  redvr  21589  frlmphllem  21752  frlmup4  21773  evls1val  22281  evls1sca  22284  smadiadetlem1  22623  smadiadetlem3lem0  22626  smadiadet  22631  d0mat2pmat  22699  chpmat0d  22795  neiptoptop  23092  upxp  23584  uptx  23586  pt1hmeo  23767  tgpconncompeqg  24073  qustgplem  24082  cnextucn  24263  psmetge0  24273  xmetge0  24305  xbln0  24375  tmsxpsval2  24500  metustid  24515  icopnfcld  24728  iocmnfcld  24729  ioo2blex  24755  tgioo  24757  blcvx  24759  xrsmopn  24774  recld2  24776  metdcn2  24801  cnmptre  24894  icchmeo  24911  icchmeoOLD  24912  cnheiborlem  24926  cnheibor  24927  lebnumii  24938  phtpyco2  24962  pi1xfrf  25026  pi1xfr  25028  pi1xfrcnvlem  25029  pi1xfrcnv  25030  pi1coghm  25034  ehleudisval  25392  ovolmge0  25451  ovolctb2  25466  nulmbl2  25510  unmbl  25511  ioombl1lem4  25535  ovolioo  25542  uniioombllem2  25557  uniioombllem4  25560  uniioombllem5  25561  uniioombllem6  25562  opnmbllem  25575  volcn  25580  i1fadd  25669  itg1addlem2  25671  i1fres  25679  itgle  25784  itgsplitioo  25812  ellimc3  25853  limcflflem  25854  limcflf  25855  limcmo  25856  limcres  25860  limciun  25868  perfdvf  25877  dvidlem  25889  dvnres  25906  dvlipcn  25972  dv11cn  25979  lhop2  25993  dvcnvrelem2  25996  tdeglem4  26038  plysub  26197  coeeulem  26202  plydiveu  26279  vieta1lem2  26292  plyexmo  26294  aaliou2b  26322  taylfval  26339  psercn  26409  pserdvlem2  26411  pserdv  26412  logdivlti  26602  efopnlem2  26639  acoscos  26876  xrlimcnp  26951  efrlim  26952  efrlimOLD  26953  lgamucov  27021  basellem9  27072  perfectlem1  27213  perfectlem2  27214  lgsqrlem4  27333  gausslemma2dlem4  27353  lgsquad2lem1  27368  lgsquad2lem2  27369  dchrisum0lem1  27500  pntlem3  27593  pntleml  27595  qrngdiv  27608  nosupbday  27690  noinfbday  27705  noetainflem4  27725  madebdaylemlrcut  27912  oniso  28284  pw2divscan4d  28457  bdayfinbndlem1  28480  ttgcontlem1  28975  brbtwn2  28996  colinearalglem4  29000  ax5seglem1  29019  axcontlem4  29058  axcontlem7  29061  wlkp1lem3  29765  wlkp1lem7  29769  wlkp1lem8  29770  pthdlem1  29857  conngrv2edg  30288  mptiffisupp  32789  elringlsm  33492  psrgsum  33731  esplyfv1  33752  esplyfv  33753  esplyfval3  33755  txomap  34018  rmulccn  34112  revpfxsfxrev  35338  cvxpconn  35464  cvxsconn  35465  cvmlift2lem10  35534  knoppcnlem10  36730  itg2gt0cn  37955  resubeqsub  42829  flt4lem7  43046  nna4b4nsq  43047  omabs2  43718  nadd2rabex  43772  enrelmap  44382  k0004lem3  44534  sineq0ALT  45321  xlimconst  46212  2ltceilhalf  47717  odz2prm2pw  47952  fmtno4prmfac  47961  lighneallem3  47996  lighneallem4a  47997  lighneallem4  47999  gpg3kgrtriexlem3  48474  fllog2  48957  2arymptfv  49039  prelrrx2b  49103  rrxsphere  49137  2sphere  49138  line2  49141  line2x  49143  line2y  49144