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  8276  oeoalem  8524  oeoelem  8526  domssex2  9067  domssex  9068  sniffsupp  9305  cantnfp1lem1  9589  en2eleq  9920  en2other2  9921  infxpenc  9930  infxpenc2lem1  9931  mappwen  10024  dfac12lem2  10057  ackbij1b  10150  fin23lem26  10237  ttukeylem5  10425  gchac  10594  wunex2  10651  00id  11310  nngt1ne1  12176  gtndiv  12571  nn01to3  12856  rpnnen1lem2  12892  nnledivrp  13021  xrre3  13088  max0sub  13113  xsubge0  13178  xrub  13229  bernneq  14154  faclbnd6  14224  bc0k  14236  brfi1indALT  14435  wrdlen2i  14867  01sqrexlem5  15171  01sqrexlem7  15173  sqreulem  15285  0.999...  15806  bpoly3  15983  fsumcube  15985  cos2t  16105  cos2tsin  16106  sin01gt0  16117  cos01gt0  16118  absefib  16125  efieq1re  16126  3dvds  16260  nno  16311  gcdcllem3  16430  gcdn0gt0  16447  divgcdodd  16639  pythagtriplem4  16749  pythagtriplem11  16755  pythagtriplem12  16756  pythagtriplem13  16757  pythagtriplem14  16758  pcfac  16829  prmreclem1  16846  vdwlem12  16922  ramval  16938  ramub2  16944  prmolelcmf  16978  prmgaplcmlem2  16982  firest  17354  yonffthlem  18207  gsumval2a  18612  prdsinvlem  18981  f1otrspeq  19378  pmtrf  19386  pmtrmvd  19387  pmtrfinv  19392  gexex  19784  cnaddinv  19802  prdsmgp  20088  zringlpirlem1  21419  zringinvg  21422  pzriprnglem10  21447  frgpcyg  21530  redvr  21574  frlmphllem  21737  frlmup4  21758  evls1val  22266  evls1sca  22269  smadiadetlem1  22608  smadiadetlem3lem0  22611  smadiadet  22616  d0mat2pmat  22684  chpmat0d  22780  neiptoptop  23077  upxp  23569  uptx  23571  pt1hmeo  23752  tgpconncompeqg  24058  qustgplem  24067  cnextucn  24248  psmetge0  24258  xmetge0  24290  xbln0  24360  tmsxpsval2  24485  metustid  24500  icopnfcld  24713  iocmnfcld  24714  ioo2blex  24740  tgioo  24742  blcvx  24744  xrsmopn  24759  recld2  24761  metdcn2  24786  cnmptre  24879  icchmeo  24896  icchmeoOLD  24897  cnheiborlem  24911  cnheibor  24912  lebnumii  24923  phtpyco2  24947  pi1xfrf  25011  pi1xfr  25013  pi1xfrcnvlem  25014  pi1xfrcnv  25015  pi1coghm  25019  ehleudisval  25377  ovolmge0  25436  ovolctb2  25451  nulmbl2  25495  unmbl  25496  ioombl1lem4  25520  ovolioo  25527  uniioombllem2  25542  uniioombllem4  25545  uniioombllem5  25546  uniioombllem6  25547  opnmbllem  25560  volcn  25565  i1fadd  25654  itg1addlem2  25656  i1fres  25664  itgle  25769  itgsplitioo  25797  ellimc3  25838  limcflflem  25839  limcflf  25840  limcmo  25841  limcres  25845  limciun  25853  perfdvf  25862  dvidlem  25874  dvnres  25891  dvlipcn  25957  dv11cn  25964  lhop2  25978  dvcnvrelem2  25981  tdeglem4  26023  plysub  26182  coeeulem  26187  plydiveu  26264  vieta1lem2  26277  plyexmo  26279  aaliou2b  26307  taylfval  26324  psercn  26394  pserdvlem2  26396  pserdv  26397  logdivlti  26587  efopnlem2  26624  acoscos  26861  xrlimcnp  26936  efrlim  26937  efrlimOLD  26938  lgamucov  27006  basellem9  27057  perfectlem1  27198  perfectlem2  27199  lgsqrlem4  27318  gausslemma2dlem4  27338  lgsquad2lem1  27353  lgsquad2lem2  27354  dchrisum0lem1  27485  pntlem3  27578  pntleml  27580  qrngdiv  27593  nosupbday  27675  noinfbday  27690  noetainflem4  27710  madebdaylemlrcut  27879  onsiso  28250  pw2divscan4d  28421  ttgcontlem1  28938  brbtwn2  28959  colinearalglem4  28963  ax5seglem1  28982  axcontlem4  29021  axcontlem7  29024  wlkp1lem3  29728  wlkp1lem7  29732  wlkp1lem8  29733  pthdlem1  29820  conngrv2edg  30251  mptiffisupp  32751  elringlsm  33453  esplyfv1  33706  esplyfv  33707  esplyfval3  33709  txomap  33970  rmulccn  34064  revpfxsfxrev  35289  cvxpconn  35415  cvxsconn  35416  cvmlift2lem10  35485  knoppcnlem10  36675  itg2gt0cn  37845  resubeqsub  42722  flt4lem7  42939  nna4b4nsq  42940  omabs2  43611  nadd2rabex  43665  enrelmap  44275  k0004lem3  44427  sineq0ALT  45214  xlimconst  46106  2ltceilhalf  47611  odz2prm2pw  47846  fmtno4prmfac  47855  lighneallem3  47890  lighneallem4a  47891  lighneallem4  47893  gpg3kgrtriexlem3  48368  fllog2  48851  2arymptfv  48933  prelrrx2b  48997  rrxsphere  49031  2sphere  49032  line2  49035  line2x  49037  line2y  49038