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  27881  onsiso  28252  pw2divscan4d  28423  ttgcontlem1  28940  brbtwn2  28961  colinearalglem4  28965  ax5seglem1  28984  axcontlem4  29023  axcontlem7  29026  wlkp1lem3  29730  wlkp1lem7  29734  wlkp1lem8  29735  pthdlem1  29822  conngrv2edg  30253  mptiffisupp  32753  elringlsm  33455  esplyfv1  33708  esplyfv  33709  esplyfval3  33711  txomap  33972  rmulccn  34066  revpfxsfxrev  35291  cvxpconn  35417  cvxsconn  35418  cvmlift2lem10  35487  knoppcnlem10  36677  itg2gt0cn  37847  resubeqsub  42721  flt4lem7  42938  nna4b4nsq  42939  omabs2  43610  nadd2rabex  43664  enrelmap  44274  k0004lem3  44426  sineq0ALT  45213  xlimconst  46105  2ltceilhalf  47610  odz2prm2pw  47845  fmtno4prmfac  47854  lighneallem3  47889  lighneallem4a  47890  lighneallem4  47892  gpg3kgrtriexlem3  48367  fllog2  48850  2arymptfv  48932  prelrrx2b  48996  rrxsphere  49030  2sphere  49031  line2  49034  line2x  49036  line2y  49037