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:  wfrlem17OLD  8339  onnseq  8358  oeoalem  8608  oeoelem  8610  domssex2  9151  domssex  9152  dif1enOLD  9176  sniffsupp  9412  cantnfp1lem1  9692  en2eleq  10022  en2other2  10023  infxpenc  10032  infxpenc2lem1  10033  mappwen  10126  dfac12lem2  10159  ackbij1b  10252  fin23lem26  10339  ttukeylem5  10527  gchac  10695  wunex2  10752  00id  11410  nngt1ne1  12269  gtndiv  12670  nn01to3  12957  rpnnen1lem2  12993  nnledivrp  13121  xrre3  13187  max0sub  13212  xsubge0  13277  xrub  13328  bernneq  14247  faclbnd6  14317  bc0k  14329  brfi1indALT  14528  wrdlen2i  14961  01sqrexlem5  15265  01sqrexlem7  15267  sqreulem  15378  0.999...  15897  bpoly3  16074  fsumcube  16076  cos2t  16196  cos2tsin  16197  sin01gt0  16208  cos01gt0  16209  absefib  16216  efieq1re  16217  3dvds  16350  nno  16401  gcdcllem3  16520  gcdn0gt0  16537  divgcdodd  16729  pythagtriplem4  16839  pythagtriplem11  16845  pythagtriplem12  16846  pythagtriplem13  16847  pythagtriplem14  16848  pcfac  16919  prmreclem1  16936  vdwlem12  17012  ramval  17028  ramub2  17034  prmolelcmf  17068  prmgaplcmlem2  17072  firest  17446  yonffthlem  18294  gsumval2a  18663  prdsinvlem  19032  f1otrspeq  19428  pmtrf  19436  pmtrmvd  19437  pmtrfinv  19442  gexex  19834  cnaddinv  19852  prdsmgp  20111  zringlpirlem1  21423  zringinvg  21426  pzriprnglem10  21451  frgpcyg  21534  redvr  21577  frlmphllem  21740  frlmup4  21761  evls1val  22258  evls1sca  22261  smadiadetlem1  22600  smadiadetlem3lem0  22603  smadiadet  22608  d0mat2pmat  22676  chpmat0d  22772  neiptoptop  23069  upxp  23561  uptx  23563  pt1hmeo  23744  tgpconncompeqg  24050  qustgplem  24059  cnextucn  24241  psmetge0  24251  xmetge0  24283  xbln0  24353  tmsxpsval2  24478  metustid  24493  icopnfcld  24706  iocmnfcld  24707  ioo2blex  24733  tgioo  24735  blcvx  24737  xrsmopn  24752  recld2  24754  metdcn2  24779  cnmptre  24872  icchmeo  24889  icchmeoOLD  24890  cnheiborlem  24904  cnheibor  24905  lebnumii  24916  phtpyco2  24940  pi1xfrf  25004  pi1xfr  25006  pi1xfrcnvlem  25007  pi1xfrcnv  25008  pi1coghm  25012  ehleudisval  25371  ovolmge0  25430  ovolctb2  25445  nulmbl2  25489  unmbl  25490  ioombl1lem4  25514  ovolioo  25521  uniioombllem2  25536  uniioombllem4  25539  uniioombllem5  25540  uniioombllem6  25541  opnmbllem  25554  volcn  25559  i1fadd  25648  itg1addlem2  25650  i1fres  25658  itgle  25763  itgsplitioo  25791  ellimc3  25832  limcflflem  25833  limcflf  25834  limcmo  25835  limcres  25839  limciun  25847  perfdvf  25856  dvidlem  25868  dvnres  25885  dvlipcn  25951  dv11cn  25958  lhop2  25972  dvcnvrelem2  25975  tdeglem4  26017  plysub  26176  coeeulem  26181  plydiveu  26258  vieta1lem2  26271  plyexmo  26273  aaliou2b  26301  taylfval  26318  psercn  26388  pserdvlem2  26390  pserdv  26391  logdivlti  26581  efopnlem2  26618  acoscos  26855  xrlimcnp  26930  efrlim  26931  efrlimOLD  26932  lgamucov  27000  basellem9  27051  perfectlem1  27192  perfectlem2  27193  lgsqrlem4  27312  gausslemma2dlem4  27332  lgsquad2lem1  27347  lgsquad2lem2  27348  dchrisum0lem1  27479  pntlem3  27572  pntleml  27574  qrngdiv  27587  nosupbday  27669  noinfbday  27684  noetainflem4  27704  madebdaylemlrcut  27862  onsiso  28221  ttgcontlem1  28864  brbtwn2  28884  colinearalglem4  28888  ax5seglem1  28907  axcontlem4  28946  axcontlem7  28949  wlkp1lem3  29655  wlkp1lem7  29659  wlkp1lem8  29660  pthdlem1  29748  conngrv2edg  30176  mptiffisupp  32670  elringlsm  33408  txomap  33865  rmulccn  33959  revpfxsfxrev  35138  cvxpconn  35264  cvxsconn  35265  cvmlift2lem10  35334  knoppcnlem10  36520  itg2gt0cn  37699  resubeqsub  42472  flt4lem7  42682  nna4b4nsq  42683  omabs2  43356  nadd2rabex  43410  enrelmap  44021  k0004lem3  44173  sineq0ALT  44961  xlimconst  45854  2ltceilhalf  47357  odz2prm2pw  47577  fmtno4prmfac  47586  lighneallem3  47621  lighneallem4a  47622  lighneallem4  47624  gpg3kgrtriexlem3  48087  fllog2  48548  2arymptfv  48630  prelrrx2b  48694  rrxsphere  48728  2sphere  48729  line2  48732  line2x  48734  line2y  48735