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  7954  onnseq  7964  oeoalem  8205  oeoelem  8207  domssex2  8661  domssex  8662  sniffsupp  8857  cantnfp1lem1  9125  en2eleq  9419  en2other2  9420  infxpenc  9429  infxpenc2lem1  9430  mappwen  9523  dfac12lem2  9555  ackbij1b  9650  fin23lem26  9736  ttukeylem5  9924  gchac  10092  wunex2  10149  00id  10804  nngt1ne1  11654  gtndiv  12047  nn01to3  12329  rpnnen1lem2  12364  nnledivrp  12489  xrre3  12552  max0sub  12577  xsubge0  12642  xrub  12693  bernneq  13586  faclbnd6  13655  bc0k  13667  brfi1indALT  13854  wrdlen2i  14295  sqrlem5  14598  sqrlem7  14600  sqreulem  14711  0.999...  15229  bpoly3  15404  fsumcube  15406  cos2t  15523  cos2tsin  15524  sin01gt0  15535  cos01gt0  15536  absefib  15543  efieq1re  15544  3dvds  15672  nno  15723  gcdcllem3  15840  gcdn0gt0  15856  divgcdodd  16044  pythagtriplem4  16146  pythagtriplem11  16152  pythagtriplem12  16153  pythagtriplem13  16154  pythagtriplem14  16155  pcfac  16225  prmreclem1  16242  vdwlem12  16318  ramval  16334  ramub2  16340  prmolelcmf  16374  prmgaplcmlem2  16378  firest  16698  yonffthlem  17524  gsumval2a  17887  prdsinvlem  18200  f1otrspeq  18567  pmtrf  18575  pmtrmvd  18576  pmtrfinv  18581  gexex  18966  cnaddinv  18984  prdsmgp  19356  zringlpirlem1  20177  zringinvg  20180  frgpcyg  20265  redvr  20306  frlmphllem  20469  frlmup4  20490  opsrtoslem2  20724  evls1val  20944  evls1sca  20947  smadiadetlem1  21267  smadiadetlem3lem0  21270  smadiadet  21275  d0mat2pmat  21343  chpmat0d  21439  neiptoptop  21736  upxp  22228  uptx  22230  pt1hmeo  22411  tgpconncompeqg  22717  qustgplem  22726  cnextucn  22909  psmetge0  22919  xmetge0  22951  xbln0  23021  tmsxpsval2  23146  metustid  23161  icopnfcld  23373  iocmnfcld  23374  ioo2blex  23399  tgioo  23401  blcvx  23403  xrsmopn  23417  recld2  23419  metdcn2  23444  cnmptre  23532  icchmeo  23546  cnheiborlem  23559  cnheibor  23560  lebnumii  23571  phtpyco2  23595  pi1xfrf  23658  pi1xfr  23660  pi1xfrcnvlem  23661  pi1xfrcnv  23662  pi1coghm  23666  ehleudisval  24023  ovolmge0  24081  ovolctb2  24096  nulmbl2  24140  unmbl  24141  ioombl1lem4  24165  ovolioo  24172  uniioombllem2  24187  uniioombllem4  24190  uniioombllem5  24191  uniioombllem6  24192  opnmbllem  24205  volcn  24210  i1fadd  24299  itg1addlem2  24301  i1fres  24309  itgle  24413  itgsplitioo  24441  ellimc3  24482  limcflflem  24483  limcflf  24484  limcmo  24485  limcres  24489  limciun  24497  perfdvf  24506  dvidlem  24518  dvnres  24534  dvlipcn  24597  dv11cn  24604  lhop2  24618  dvcnvrelem2  24621  plysub  24816  coeeulem  24821  plydiveu  24894  vieta1lem2  24907  plyexmo  24909  aaliou2b  24937  taylfval  24954  psercn  25021  pserdvlem2  25023  pserdv  25024  logdivlti  25211  efopnlem2  25248  acoscos  25479  xrlimcnp  25554  efrlim  25555  lgamucov  25623  basellem9  25674  perfectlem1  25813  perfectlem2  25814  lgsqrlem4  25933  gausslemma2dlem4  25953  lgsquad2lem1  25968  lgsquad2lem2  25969  dchrisum0lem1  26100  pntlem3  26193  pntleml  26195  qrngdiv  26208  ttgcontlem1  26679  brbtwn2  26699  colinearalglem4  26703  ax5seglem1  26722  axcontlem4  26761  axcontlem7  26764  wlkp1lem3  27465  wlkp1lem7  27469  wlkp1lem8  27470  pthdlem1  27555  conngrv2edg  27980  elringlsm  31000  txomap  31187  revpfxsfxrev  32475  cvmlift2lem10  32672  nosupbday  33318  itg2gt0cn  35112  resubeqsub  39566  enrelmap  40698  k0004lem3  40852  sineq0ALT  41643  xlimconst  42467  odz2prm2pw  44080  fmtno4prmfac  44089  lighneallem3  44125  lighneallem4a  44126  lighneallem4  44128  fllog2  44982  2arymptfv  45064  prelrrx2b  45128  rrxsphere  45162  2sphere  45163  line2  45166  line2x  45168  line2y  45169