Theorem mp3an2i 1466

Description: mp3an 1461 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 1448	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	1, 2, 5	syl2anc 584	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  wfrlem17OLD  8321  onnseq  8340  oeoalem  8592  oeoelem  8594  domssex2  9133  domssex  9134  dif1enOLD  9158  sniffsupp  9391  cantnfp1lem1  9669  en2eleq  9999  en2other2  10000  infxpenc  10009  infxpenc2lem1  10010  mappwen  10103  dfac12lem2  10135  ackbij1b  10230  fin23lem26  10316  ttukeylem5  10504  gchac  10672  wunex2  10729  00id  11385  nngt1ne1  12237  gtndiv  12635  nn01to3  12921  rpnnen1lem2  12957  nnledivrp  13082  xrre3  13146  max0sub  13171  xsubge0  13236  xrub  13287  bernneq  14188  faclbnd6  14255  bc0k  14267  brfi1indALT  14457  wrdlen2i  14889  01sqrexlem5  15189  01sqrexlem7  15191  sqreulem  15302  0.999...  15823  bpoly3  15998  fsumcube  16000  cos2t  16117  cos2tsin  16118  sin01gt0  16129  cos01gt0  16130  absefib  16137  efieq1re  16138  3dvds  16270  nno  16321  gcdcllem3  16438  gcdn0gt0  16455  divgcdodd  16643  pythagtriplem4  16748  pythagtriplem11  16754  pythagtriplem12  16755  pythagtriplem13  16756  pythagtriplem14  16757  pcfac  16828  prmreclem1  16845  vdwlem12  16921  ramval  16937  ramub2  16943  prmolelcmf  16977  prmgaplcmlem2  16981  firest  17374  yonffthlem  18231  gsumval2a  18600  prdsinvlem  18928  f1otrspeq  19309  pmtrf  19317  pmtrmvd  19318  pmtrfinv  19323  gexex  19715  cnaddinv  19733  prdsmgp  20125  zringlpirlem1  21023  zringinvg  21026  frgpcyg  21120  redvr  21161  frlmphllem  21326  frlmup4  21347  evls1val  21830  evls1sca  21833  smadiadetlem1  22155  smadiadetlem3lem0  22158  smadiadet  22163  d0mat2pmat  22231  chpmat0d  22327  neiptoptop  22626  upxp  23118  uptx  23120  pt1hmeo  23301  tgpconncompeqg  23607  qustgplem  23616  cnextucn  23799  psmetge0  23809  xmetge0  23841  xbln0  23911  tmsxpsval2  24039  metustid  24054  icopnfcld  24275  iocmnfcld  24276  ioo2blex  24301  tgioo  24303  blcvx  24305  xrsmopn  24319  recld2  24321  metdcn2  24346  cnmptre  24434  icchmeo  24448  cnheiborlem  24461  cnheibor  24462  lebnumii  24473  phtpyco2  24497  pi1xfrf  24560  pi1xfr  24562  pi1xfrcnvlem  24563  pi1xfrcnv  24564  pi1coghm  24568  ehleudisval  24927  ovolmge0  24985  ovolctb2  25000  nulmbl2  25044  unmbl  25045  ioombl1lem4  25069  ovolioo  25076  uniioombllem2  25091  uniioombllem4  25094  uniioombllem5  25095  uniioombllem6  25096  opnmbllem  25109  volcn  25114  i1fadd  25203  itg1addlem2  25205  i1fres  25214  itgle  25318  itgsplitioo  25346  ellimc3  25387  limcflflem  25388  limcflf  25389  limcmo  25390  limcres  25394  limciun  25402  perfdvf  25411  dvidlem  25423  dvnres  25439  dvlipcn  25502  dv11cn  25509  lhop2  25523  dvcnvrelem2  25526  tdeglem4  25568  plysub  25724  coeeulem  25729  plydiveu  25802  vieta1lem2  25815  plyexmo  25817  aaliou2b  25845  taylfval  25862  psercn  25929  pserdvlem2  25931  pserdv  25932  logdivlti  26119  efopnlem2  26156  acoscos  26387  xrlimcnp  26462  efrlim  26463  lgamucov  26531  basellem9  26582  perfectlem1  26721  perfectlem2  26722  lgsqrlem4  26841  gausslemma2dlem4  26861  lgsquad2lem1  26876  lgsquad2lem2  26877  dchrisum0lem1  27008  pntlem3  27101  pntleml  27103  qrngdiv  27116  nosupbday  27197  noinfbday  27212  noetainflem4  27232  madebdaylemlrcut  27382  ttgcontlem1  28131  brbtwn2  28152  colinearalglem4  28156  ax5seglem1  28175  axcontlem4  28214  axcontlem7  28217  wlkp1lem3  28921  wlkp1lem7  28925  wlkp1lem8  28926  pthdlem1  29012  conngrv2edg  29437  mptiffisupp  31902  elringlsm  32491  txomap  32802  revpfxsfxrev  34094  cvmlift2lem10  34291  gg-icchmeo  35158  itg2gt0cn  36531  resubeqsub  41298  flt4lem7  41397  nna4b4nsq  41398  omabs2  42067  nadd2rabex  42121  enrelmap  42733  k0004lem3  42885  sineq0ALT  43683  xlimconst  44527  odz2prm2pw  46217  fmtno4prmfac  46226  lighneallem3  46261  lighneallem4a  46262  lighneallem4  46264  fllog2  47207  2arymptfv  47289  prelrrx2b  47353  rrxsphere  47387  2sphere  47388  line2  47391  line2x  47393  line2y  47394