Theorem mp3an2i 1468

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  onnseq  8267  oeoalem  8514  oeoelem  8516  domssex2  9054  domssex  9055  sniffsupp  9290  cantnfp1lem1  9574  en2eleq  9902  en2other2  9903  infxpenc  9912  infxpenc2lem1  9913  mappwen  10006  dfac12lem2  10039  ackbij1b  10132  fin23lem26  10219  ttukeylem5  10407  gchac  10575  wunex2  10632  00id  11291  nngt1ne1  12157  gtndiv  12553  nn01to3  12842  rpnnen1lem2  12878  nnledivrp  13007  xrre3  13073  max0sub  13098  xsubge0  13163  xrub  13214  bernneq  14136  faclbnd6  14206  bc0k  14218  brfi1indALT  14417  wrdlen2i  14849  01sqrexlem5  15153  01sqrexlem7  15155  sqreulem  15267  0.999...  15788  bpoly3  15965  fsumcube  15967  cos2t  16087  cos2tsin  16088  sin01gt0  16099  cos01gt0  16100  absefib  16107  efieq1re  16108  3dvds  16242  nno  16293  gcdcllem3  16412  gcdn0gt0  16429  divgcdodd  16621  pythagtriplem4  16731  pythagtriplem11  16737  pythagtriplem12  16738  pythagtriplem13  16739  pythagtriplem14  16740  pcfac  16811  prmreclem1  16828  vdwlem12  16904  ramval  16920  ramub2  16926  prmolelcmf  16960  prmgaplcmlem2  16964  firest  17336  yonffthlem  18188  gsumval2a  18559  prdsinvlem  18928  f1otrspeq  19326  pmtrf  19334  pmtrmvd  19335  pmtrfinv  19340  gexex  19732  cnaddinv  19750  prdsmgp  20036  zringlpirlem1  21369  zringinvg  21372  pzriprnglem10  21397  frgpcyg  21480  redvr  21524  frlmphllem  21687  frlmup4  21708  evls1val  22205  evls1sca  22208  smadiadetlem1  22547  smadiadetlem3lem0  22550  smadiadet  22555  d0mat2pmat  22623  chpmat0d  22719  neiptoptop  23016  upxp  23508  uptx  23510  pt1hmeo  23691  tgpconncompeqg  23997  qustgplem  24006  cnextucn  24188  psmetge0  24198  xmetge0  24230  xbln0  24300  tmsxpsval2  24425  metustid  24440  icopnfcld  24653  iocmnfcld  24654  ioo2blex  24680  tgioo  24682  blcvx  24684  xrsmopn  24699  recld2  24701  metdcn2  24726  cnmptre  24819  icchmeo  24836  icchmeoOLD  24837  cnheiborlem  24851  cnheibor  24852  lebnumii  24863  phtpyco2  24887  pi1xfrf  24951  pi1xfr  24953  pi1xfrcnvlem  24954  pi1xfrcnv  24955  pi1coghm  24959  ehleudisval  25317  ovolmge0  25376  ovolctb2  25391  nulmbl2  25435  unmbl  25436  ioombl1lem4  25460  ovolioo  25467  uniioombllem2  25482  uniioombllem4  25485  uniioombllem5  25486  uniioombllem6  25487  opnmbllem  25500  volcn  25505  i1fadd  25594  itg1addlem2  25596  i1fres  25604  itgle  25709  itgsplitioo  25737  ellimc3  25778  limcflflem  25779  limcflf  25780  limcmo  25781  limcres  25785  limciun  25793  perfdvf  25802  dvidlem  25814  dvnres  25831  dvlipcn  25897  dv11cn  25904  lhop2  25918  dvcnvrelem2  25921  tdeglem4  25963  plysub  26122  coeeulem  26127  plydiveu  26204  vieta1lem2  26217  plyexmo  26219  aaliou2b  26247  taylfval  26264  psercn  26334  pserdvlem2  26336  pserdv  26337  logdivlti  26527  efopnlem2  26564  acoscos  26801  xrlimcnp  26876  efrlim  26877  efrlimOLD  26878  lgamucov  26946  basellem9  26997  perfectlem1  27138  perfectlem2  27139  lgsqrlem4  27258  gausslemma2dlem4  27278  lgsquad2lem1  27293  lgsquad2lem2  27294  dchrisum0lem1  27425  pntlem3  27518  pntleml  27520  qrngdiv  27533  nosupbday  27615  noinfbday  27630  noetainflem4  27650  madebdaylemlrcut  27815  onsiso  28176  pw2divscan4d  28338  ttgcontlem1  28834  brbtwn2  28854  colinearalglem4  28858  ax5seglem1  28877  axcontlem4  28916  axcontlem7  28919  wlkp1lem3  29623  wlkp1lem7  29627  wlkp1lem8  29628  pthdlem1  29715  conngrv2edg  30143  mptiffisupp  32643  elringlsm  33339  txomap  33817  rmulccn  33911  revpfxsfxrev  35109  cvxpconn  35235  cvxsconn  35236  cvmlift2lem10  35305  knoppcnlem10  36496  itg2gt0cn  37675  resubeqsub  42423  flt4lem7  42652  nna4b4nsq  42653  omabs2  43325  nadd2rabex  43379  enrelmap  43990  k0004lem3  44142  sineq0ALT  44930  xlimconst  45826  2ltceilhalf  47332  odz2prm2pw  47567  fmtno4prmfac  47576  lighneallem3  47611  lighneallem4a  47612  lighneallem4  47614  gpg3kgrtriexlem3  48089  fllog2  48573  2arymptfv  48655  prelrrx2b  48719  rrxsphere  48753  2sphere  48754  line2  48757  line2x  48759  line2y  48760