Theorem mp3an2i 1465

Description: mp3an 1460 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 1447	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  wfrlem17OLD  8165  onnseq  8184  oeoalem  8436  oeoelem  8438  domssex2  8933  domssex  8934  dif1en  8954  sniffsupp  9168  cantnfp1lem1  9445  en2eleq  9773  en2other2  9774  infxpenc  9783  infxpenc2lem1  9784  mappwen  9877  dfac12lem2  9909  ackbij1b  10004  fin23lem26  10090  ttukeylem5  10278  gchac  10446  wunex2  10503  00id  11159  nngt1ne1  12011  gtndiv  12406  nn01to3  12690  rpnnen1lem2  12726  nnledivrp  12851  xrre3  12914  max0sub  12939  xsubge0  13004  xrub  13055  bernneq  13953  faclbnd6  14022  bc0k  14034  brfi1indALT  14223  wrdlen2i  14664  sqrlem5  14967  sqrlem7  14969  sqreulem  15080  0.999...  15602  bpoly3  15777  fsumcube  15779  cos2t  15896  cos2tsin  15897  sin01gt0  15908  cos01gt0  15909  absefib  15916  efieq1re  15917  3dvds  16049  nno  16100  gcdcllem3  16217  gcdn0gt0  16234  divgcdodd  16424  pythagtriplem4  16529  pythagtriplem11  16535  pythagtriplem12  16536  pythagtriplem13  16537  pythagtriplem14  16538  pcfac  16609  prmreclem1  16626  vdwlem12  16702  ramval  16718  ramub2  16724  prmolelcmf  16758  prmgaplcmlem2  16762  firest  17152  yonffthlem  18009  gsumval2a  18378  prdsinvlem  18693  f1otrspeq  19064  pmtrf  19072  pmtrmvd  19073  pmtrfinv  19078  gexex  19463  cnaddinv  19481  prdsmgp  19858  zringlpirlem1  20693  zringinvg  20696  frgpcyg  20790  redvr  20831  frlmphllem  20996  frlmup4  21017  evls1val  21495  evls1sca  21498  smadiadetlem1  21820  smadiadetlem3lem0  21823  smadiadet  21828  d0mat2pmat  21896  chpmat0d  21992  neiptoptop  22291  upxp  22783  uptx  22785  pt1hmeo  22966  tgpconncompeqg  23272  qustgplem  23281  cnextucn  23464  psmetge0  23474  xmetge0  23506  xbln0  23576  tmsxpsval2  23704  metustid  23719  icopnfcld  23940  iocmnfcld  23941  ioo2blex  23966  tgioo  23968  blcvx  23970  xrsmopn  23984  recld2  23986  metdcn2  24011  cnmptre  24099  icchmeo  24113  cnheiborlem  24126  cnheibor  24127  lebnumii  24138  phtpyco2  24162  pi1xfrf  24225  pi1xfr  24227  pi1xfrcnvlem  24228  pi1xfrcnv  24229  pi1coghm  24233  ehleudisval  24592  ovolmge0  24650  ovolctb2  24665  nulmbl2  24709  unmbl  24710  ioombl1lem4  24734  ovolioo  24741  uniioombllem2  24756  uniioombllem4  24759  uniioombllem5  24760  uniioombllem6  24761  opnmbllem  24774  volcn  24779  i1fadd  24868  itg1addlem2  24870  i1fres  24879  itgle  24983  itgsplitioo  25011  ellimc3  25052  limcflflem  25053  limcflf  25054  limcmo  25055  limcres  25059  limciun  25067  perfdvf  25076  dvidlem  25088  dvnres  25104  dvlipcn  25167  dv11cn  25174  lhop2  25188  dvcnvrelem2  25191  tdeglem4  25233  plysub  25389  coeeulem  25394  plydiveu  25467  vieta1lem2  25480  plyexmo  25482  aaliou2b  25510  taylfval  25527  psercn  25594  pserdvlem2  25596  pserdv  25597  logdivlti  25784  efopnlem2  25821  acoscos  26052  xrlimcnp  26127  efrlim  26128  lgamucov  26196  basellem9  26247  perfectlem1  26386  perfectlem2  26387  lgsqrlem4  26506  gausslemma2dlem4  26526  lgsquad2lem1  26541  lgsquad2lem2  26542  dchrisum0lem1  26673  pntlem3  26766  pntleml  26768  qrngdiv  26781  ttgcontlem1  27261  brbtwn2  27282  colinearalglem4  27286  ax5seglem1  27305  axcontlem4  27344  axcontlem7  27347  wlkp1lem3  28052  wlkp1lem7  28056  wlkp1lem8  28057  pthdlem1  28143  conngrv2edg  28568  elringlsm  31590  txomap  31793  revpfxsfxrev  33086  cvmlift2lem10  33283  nosupbday  33917  noinfbday  33932  noetainflem4  33952  madebdaylemlrcut  34088  itg2gt0cn  35841  resubeqsub  40418  flt4lem7  40503  nna4b4nsq  40504  enrelmap  41612  k0004lem3  41766  sineq0ALT  42564  xlimconst  43373  odz2prm2pw  45026  fmtno4prmfac  45035  lighneallem3  45070  lighneallem4a  45071  lighneallem4  45073  fllog2  45925  2arymptfv  46007  prelrrx2b  46071  rrxsphere  46105  2sphere  46106  line2  46109  line2x  46111  line2y  46112