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  8278  oeoalem  8526  oeoelem  8528  domssex2  9069  domssex  9070  sniffsupp  9307  cantnfp1lem1  9591  en2eleq  9922  en2other2  9923  infxpenc  9932  infxpenc2lem1  9933  mappwen  10026  dfac12lem2  10059  ackbij1b  10152  fin23lem26  10239  ttukeylem5  10427  gchac  10596  wunex2  10653  00id  11312  nngt1ne1  12178  gtndiv  12573  nn01to3  12858  rpnnen1lem2  12894  nnledivrp  13023  xrre3  13090  max0sub  13115  xsubge0  13180  xrub  13231  bernneq  14156  faclbnd6  14226  bc0k  14238  brfi1indALT  14437  wrdlen2i  14869  01sqrexlem5  15173  01sqrexlem7  15175  sqreulem  15287  0.999...  15808  bpoly3  15985  fsumcube  15987  cos2t  16107  cos2tsin  16108  sin01gt0  16119  cos01gt0  16120  absefib  16127  efieq1re  16128  3dvds  16262  nno  16313  gcdcllem3  16432  gcdn0gt0  16449  divgcdodd  16641  pythagtriplem4  16751  pythagtriplem11  16757  pythagtriplem12  16758  pythagtriplem13  16759  pythagtriplem14  16760  pcfac  16831  prmreclem1  16848  vdwlem12  16924  ramval  16940  ramub2  16946  prmolelcmf  16980  prmgaplcmlem2  16984  firest  17356  yonffthlem  18209  gsumval2a  18614  prdsinvlem  18983  f1otrspeq  19380  pmtrf  19388  pmtrmvd  19389  pmtrfinv  19394  gexex  19786  cnaddinv  19804  prdsmgp  20090  zringlpirlem1  21421  zringinvg  21424  pzriprnglem10  21449  frgpcyg  21532  redvr  21576  frlmphllem  21739  frlmup4  21760  evls1val  22268  evls1sca  22271  smadiadetlem1  22610  smadiadetlem3lem0  22613  smadiadet  22618  d0mat2pmat  22686  chpmat0d  22782  neiptoptop  23079  upxp  23571  uptx  23573  pt1hmeo  23754  tgpconncompeqg  24060  qustgplem  24069  cnextucn  24250  psmetge0  24260  xmetge0  24292  xbln0  24362  tmsxpsval2  24487  metustid  24502  icopnfcld  24715  iocmnfcld  24716  ioo2blex  24742  tgioo  24744  blcvx  24746  xrsmopn  24761  recld2  24763  metdcn2  24788  cnmptre  24881  icchmeo  24898  icchmeoOLD  24899  cnheiborlem  24913  cnheibor  24914  lebnumii  24925  phtpyco2  24949  pi1xfrf  25013  pi1xfr  25015  pi1xfrcnvlem  25016  pi1xfrcnv  25017  pi1coghm  25021  ehleudisval  25379  ovolmge0  25438  ovolctb2  25453  nulmbl2  25497  unmbl  25498  ioombl1lem4  25522  ovolioo  25529  uniioombllem2  25544  uniioombllem4  25547  uniioombllem5  25548  uniioombllem6  25549  opnmbllem  25562  volcn  25567  i1fadd  25656  itg1addlem2  25658  i1fres  25666  itgle  25771  itgsplitioo  25799  ellimc3  25840  limcflflem  25841  limcflf  25842  limcmo  25843  limcres  25847  limciun  25855  perfdvf  25864  dvidlem  25876  dvnres  25893  dvlipcn  25959  dv11cn  25966  lhop2  25980  dvcnvrelem2  25983  tdeglem4  26025  plysub  26184  coeeulem  26189  plydiveu  26266  vieta1lem2  26279  plyexmo  26281  aaliou2b  26309  taylfval  26326  psercn  26396  pserdvlem2  26398  pserdv  26399  logdivlti  26589  efopnlem2  26626  acoscos  26863  xrlimcnp  26938  efrlim  26939  efrlimOLD  26940  lgamucov  27008  basellem9  27059  perfectlem1  27200  perfectlem2  27201  lgsqrlem4  27320  gausslemma2dlem4  27340  lgsquad2lem1  27355  lgsquad2lem2  27356  dchrisum0lem1  27487  pntlem3  27580  pntleml  27582  qrngdiv  27595  nosupbday  27677  noinfbday  27692  noetainflem4  27712  madebdaylemlrcut  27899  oniso  28271  pw2divscan4d  28444  bdayfinbndlem1  28467  ttgcontlem1  28961  brbtwn2  28982  colinearalglem4  28986  ax5seglem1  29005  axcontlem4  29044  axcontlem7  29047  wlkp1lem3  29751  wlkp1lem7  29755  wlkp1lem8  29756  pthdlem1  29843  conngrv2edg  30274  mptiffisupp  32774  elringlsm  33476  esplyfv1  33729  esplyfv  33730  esplyfval3  33732  txomap  33993  rmulccn  34087  revpfxsfxrev  35312  cvxpconn  35438  cvxsconn  35439  cvmlift2lem10  35508  knoppcnlem10  36704  itg2gt0cn  37878  resubeqsub  42752  flt4lem7  42969  nna4b4nsq  42970  omabs2  43641  nadd2rabex  43695  enrelmap  44305  k0004lem3  44457  sineq0ALT  45244  xlimconst  46136  2ltceilhalf  47641  odz2prm2pw  47876  fmtno4prmfac  47885  lighneallem3  47920  lighneallem4a  47921  lighneallem4  47923  gpg3kgrtriexlem3  48398  fllog2  48881  2arymptfv  48963  prelrrx2b  49027  rrxsphere  49061  2sphere  49062  line2  49065  line2x  49067  line2y  49068