Theorem mp3an2i 1463

Description: mp3an 1458 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 1445	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	1, 2, 5	syl2anc 587	1 ⊢ (𝜓 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  wfrlem17  7986  onnseq  7996  oeoalem  8237  oeoelem  8239  domssex2  8704  domssex  8705  dif1en  8738  sniffsupp  8902  cantnfp1lem1  9179  en2eleq  9473  en2other2  9474  infxpenc  9483  infxpenc2lem1  9484  mappwen  9577  dfac12lem2  9609  ackbij1b  9704  fin23lem26  9790  ttukeylem5  9978  gchac  10146  wunex2  10203  00id  10858  nngt1ne1  11708  gtndiv  12103  nn01to3  12386  rpnnen1lem2  12422  nnledivrp  12547  xrre3  12610  max0sub  12635  xsubge0  12700  xrub  12751  bernneq  13645  faclbnd6  13714  bc0k  13726  brfi1indALT  13915  wrdlen2i  14356  sqrlem5  14659  sqrlem7  14661  sqreulem  14772  0.999...  15290  bpoly3  15465  fsumcube  15467  cos2t  15584  cos2tsin  15585  sin01gt0  15596  cos01gt0  15597  absefib  15604  efieq1re  15605  3dvds  15737  nno  15788  gcdcllem3  15905  gcdn0gt0  15922  divgcdodd  16111  pythagtriplem4  16216  pythagtriplem11  16222  pythagtriplem12  16223  pythagtriplem13  16224  pythagtriplem14  16225  pcfac  16295  prmreclem1  16312  vdwlem12  16388  ramval  16404  ramub2  16410  prmolelcmf  16444  prmgaplcmlem2  16448  firest  16769  yonffthlem  17603  gsumval2a  17966  prdsinvlem  18280  f1otrspeq  18647  pmtrf  18655  pmtrmvd  18656  pmtrfinv  18661  gexex  19046  cnaddinv  19064  prdsmgp  19436  zringlpirlem1  20257  zringinvg  20260  frgpcyg  20346  redvr  20387  frlmphllem  20550  frlmup4  20571  evls1val  21044  evls1sca  21047  smadiadetlem1  21367  smadiadetlem3lem0  21370  smadiadet  21375  d0mat2pmat  21443  chpmat0d  21539  neiptoptop  21836  upxp  22328  uptx  22330  pt1hmeo  22511  tgpconncompeqg  22817  qustgplem  22826  cnextucn  23009  psmetge0  23019  xmetge0  23051  xbln0  23121  tmsxpsval2  23246  metustid  23261  icopnfcld  23474  iocmnfcld  23475  ioo2blex  23500  tgioo  23502  blcvx  23504  xrsmopn  23518  recld2  23520  metdcn2  23545  cnmptre  23633  icchmeo  23647  cnheiborlem  23660  cnheibor  23661  lebnumii  23672  phtpyco2  23696  pi1xfrf  23759  pi1xfr  23761  pi1xfrcnvlem  23762  pi1xfrcnv  23763  pi1coghm  23767  ehleudisval  24124  ovolmge0  24182  ovolctb2  24197  nulmbl2  24241  unmbl  24242  ioombl1lem4  24266  ovolioo  24273  uniioombllem2  24288  uniioombllem4  24291  uniioombllem5  24292  uniioombllem6  24293  opnmbllem  24306  volcn  24311  i1fadd  24400  itg1addlem2  24402  i1fres  24410  itgle  24514  itgsplitioo  24542  ellimc3  24583  limcflflem  24584  limcflf  24585  limcmo  24586  limcres  24590  limciun  24598  perfdvf  24607  dvidlem  24619  dvnres  24635  dvlipcn  24698  dv11cn  24705  lhop2  24719  dvcnvrelem2  24722  tdeglem4  24764  plysub  24920  coeeulem  24925  plydiveu  24998  vieta1lem2  25011  plyexmo  25013  aaliou2b  25041  taylfval  25058  psercn  25125  pserdvlem2  25127  pserdv  25128  logdivlti  25315  efopnlem2  25352  acoscos  25583  xrlimcnp  25658  efrlim  25659  lgamucov  25727  basellem9  25778  perfectlem1  25917  perfectlem2  25918  lgsqrlem4  26037  gausslemma2dlem4  26057  lgsquad2lem1  26072  lgsquad2lem2  26073  dchrisum0lem1  26204  pntlem3  26297  pntleml  26299  qrngdiv  26312  ttgcontlem1  26783  brbtwn2  26803  colinearalglem4  26807  ax5seglem1  26826  axcontlem4  26865  axcontlem7  26868  wlkp1lem3  27569  wlkp1lem7  27573  wlkp1lem8  27574  pthdlem1  27659  conngrv2edg  28084  elringlsm  31106  txomap  31309  revpfxsfxrev  32597  cvmlift2lem10  32794  nosupbday  33497  noinfbday  33512  noetainflem4  33532  madebdaylemlrcut  33662  itg2gt0cn  35418  resubeqsub  39936  nna4b4nsq  40017  enrelmap  41099  k0004lem3  41253  sineq0ALT  42044  xlimconst  42861  odz2prm2pw  44476  fmtno4prmfac  44485  lighneallem3  44520  lighneallem4a  44521  lighneallem4  44523  fllog2  45375  2arymptfv  45457  prelrrx2b  45521  rrxsphere  45555  2sphere  45556  line2  45559  line2x  45561  line2y  45562