Theorem mp3an2i 1475

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  onnseq  8278  oeoalem  8526  oeoelem  8528  domssex2  9069  domssex  9070  sniffsupp  9307  cantnfp1lem1  9594  en2eleq  9925  en2other2  9926  infxpenc  9935  infxpenc2lem1  9936  mappwen  10029  dfac12lem2  10062  ackbij1b  10155  fin23lem26  10242  ttukeylem5  10430  gchac  10599  wunex2  10656  00id  11316  nngt1ne1  12201  gtndiv  12601  nn01to3  12886  rpnnen1lem2  12922  nnledivrp  13051  xrre3  13118  max0sub  13143  xsubge0  13208  xrub  13259  bernneq  14186  faclbnd6  14256  bc0k  14268  brfi1indALT  14467  wrdlen2i  14899  01sqrexlem5  15203  01sqrexlem7  15205  sqreulem  15317  0.999...  15841  bpoly3  16018  fsumcube  16020  cos2t  16140  cos2tsin  16141  sin01gt0  16152  cos01gt0  16153  absefib  16160  efieq1re  16161  3dvds  16295  nno  16346  gcdcllem3  16465  gcdn0gt0  16482  divgcdodd  16675  pythagtriplem4  16785  pythagtriplem11  16791  pythagtriplem12  16792  pythagtriplem13  16793  pythagtriplem14  16794  pcfac  16865  prmreclem1  16882  vdwlem12  16958  ramval  16974  ramub2  16980  prmolelcmf  17014  prmgaplcmlem2  17018  firest  17390  yonffthlem  18243  gsumval2a  18648  prdsinvlem  19020  f1otrspeq  19417  pmtrf  19425  pmtrmvd  19426  pmtrfinv  19431  gexex  19823  cnaddinv  19841  prdsmgp  20127  zringlpirlem1  21441  zringinvg  21444  pzriprnglem10  21469  frgpcyg  21552  redvr  21596  frlmphllem  21759  frlmup4  21780  evls1val  22310  evls1sca  22313  smadiadetlem1  22649  smadiadetlem3lem0  22652  smadiadet  22657  d0mat2pmat  22725  chpmat0d  22821  neiptoptop  23118  upxp  23610  uptx  23612  pt1hmeo  23793  tgpconncompeqg  24099  qustgplem  24108  cnextucn  24289  psmetge0  24299  xmetge0  24331  xbln0  24401  tmsxpsval2  24526  metustid  24541  icopnfcld  24754  iocmnfcld  24755  ioo2blex  24781  tgioo  24783  blcvx  24785  xrsmopn  24800  recld2  24802  metdcn2  24827  cnmptre  24916  icchmeo  24930  cnheiborlem  24943  cnheibor  24944  lebnumii  24955  phtpyco2  24979  pi1xfrf  25042  pi1xfr  25044  pi1xfrcnvlem  25045  pi1xfrcnv  25046  pi1coghm  25050  ehleudisval  25408  ovolmge0  25466  ovolctb2  25481  nulmbl2  25525  unmbl  25526  ioombl1lem4  25550  ovolioo  25557  uniioombllem2  25572  uniioombllem4  25575  uniioombllem5  25576  uniioombllem6  25577  opnmbllem  25590  volcn  25595  i1fadd  25684  itg1addlem2  25686  i1fres  25694  itgle  25799  itgsplitioo  25827  ellimc3  25868  limcflflem  25869  limcflf  25870  limcmo  25871  limcres  25875  limciun  25883  perfdvf  25892  dvidlem  25904  dvnres  25920  dvlipcn  25983  dv11cn  25990  lhop2  26004  dvcnvrelem2  26007  tdeglem4  26047  plysub  26206  coeeulem  26211  plydiveu  26286  vieta1lem2  26299  plyexmo  26301  aaliou2b  26329  taylfval  26346  psercn  26413  pserdvlem2  26415  pserdv  26416  logdivlti  26606  efopnlem2  26643  acoscos  26879  xrlimcnp  26954  efrlim  26955  lgamucov  27023  basellem9  27074  perfectlem1  27214  perfectlem2  27215  lgsqrlem4  27334  gausslemma2dlem4  27354  lgsquad2lem1  27369  lgsquad2lem2  27370  dchrisum0lem1  27501  pntlem3  27594  pntleml  27596  qrngdiv  27609  nosupbday  27691  noinfbday  27706  noetainflem4  27726  madebdaylemlrcut  27913  oniso  28285  pw2divscan4d  28458  bdayfinbndlem1  28481  ttgcontlem1  28975  brbtwn2  28996  colinearalglem4  29000  ax5seglem1  29019  axcontlem4  29058  axcontlem7  29061  wlkp1lem3  29764  wlkp1lem7  29768  wlkp1lem8  29769  pthdlem1  29856  conngrv2edg  30287  mptiffisupp  32789  elringlsm  33480  0mplrim  33710  psrgsum  33744  esplyfv1  33765  esplyfv  33766  esplyfval3  33768  txomap  34030  rmulccn  34124  revpfxsfxrev  35359  cvxpconn  35485  cvxsconn  35486  cvmlift2lem10  35555  knoppcnlem10  36823  itg2gt0cn  38057  resubeqsub  42922  flt4lem7  43124  nna4b4nsq  43125  omabs2  43792  nadd2rabex  43846  enrelmap  44456  k0004lem3  44608  sineq0ALT  45395  xlimconst  46282  2ltceilhalf  47809  2timesltsqm1  47856  odz2prm2pw  48055  fmtno4prmfac  48064  lighneallem3  48099  lighneallem4a  48100  lighneallem4  48102  gpg3kgrtriexlem3  48590  fllog2  49073  2arymptfv  49155  prelrrx2b  49219  rrxsphere  49253  2sphere  49254  line2  49257  line2x  49259  line2y  49260