Theorem mp3an2i 1495

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  onnseq  8331  oeoalem  8584  oeoelem  8586  domssex2  9135  domssex  9136  sniffsupp  9370  cantnfp1lem1  9657  en2eleq  10044  en2other2  10045  infxpenc  10054  infxpenc2lem1  10055  mappwen  10148  dfac12lem2  10180  ackbij1b  10273  fin23lem26  10360  ttukeylem5  10548  gchac  10723  wunex2  10780  00id  11442  nngt1ne1  12322  gtndiv  12731  nn01to3  13023  rpnnen1lem2  13060  nnledivrp  13189  xrre3  13256  max0sub  13281  xsubge0  13346  xrub  13397  bernneq  14326  faclbnd6  14396  bc0k  14408  brfi1indALT  14608  revpfxsfxrev  14870  wrdlen2i  15046  01sqrexlem5  15366  01sqrexlem7  15368  sqreulem  15480  0.999...  16003  bpoly3  16177  fsumcube  16179  cos2t  16299  cos2tsin  16300  sin01gt0  16311  cos01gt0  16312  absefib  16319  efieq1re  16320  3dvds  16454  nno  16505  gcdcllem3  16624  gcdn0gt0  16641  divgcdodd  16834  pythagtriplem4  16944  pythagtriplem11  16950  pythagtriplem12  16951  pythagtriplem13  16952  pythagtriplem14  16953  pcfac  17024  prmreclem1  17041  vdwlem12  17117  ramval  17133  ramub2  17139  prmolelcmf  17173  prmgaplcmlem2  17177  firest  17550  yonffthlem  18403  gsumval2a  18821  prdsinvlem  19206  f1otrspeq  19608  pmtrf  19616  pmtrmvd  19617  pmtrfinv  19622  gexex  20014  cnaddinv  20032  prdsmgp  20318  elmgplsm  20319  zringlpirlem1  21715  zringinvg  21718  pzriprnglem10  21743  frgpcyg  21826  redvr  21870  frlmphllem  22033  frlmup4  22054  evls1val  22585  evls1sca  22588  smadiadetlem1  22924  smadiadetlem3lem0  22927  smadiadet  22932  d0mat2pmat  23003  chpmat0d  23099  neiptoptop  23396  upxp  23889  uptx  23891  pt1hmeo  24072  tgpconncompeqg  24378  qustgplem  24387  cnextucn  24568  psmetge0  24578  xmetge0  24610  xbln0  24680  tmsxpsval2  24805  metustid  24820  icopnfcld  25033  iocmnfcld  25034  ioo2blex  25060  tgioo  25062  blcvx  25064  xrsmopn  25079  recld2  25081  metdcn2  25106  cnmptre  25195  icchmeo  25209  cnheiborlem  25222  cnheibor  25223  lebnumii  25234  phtpyco2  25258  pi1xfrf  25321  pi1xfr  25323  pi1xfrcnvlem  25324  pi1xfrcnv  25325  pi1coghm  25329  ehleudisval  25687  ovolmge0  25745  ovolctb2  25760  nulmbl2  25804  unmbl  25805  ioombl1lem4  25829  ovolioo  25836  uniioombllem2  25851  uniioombllem4  25854  uniioombllem5  25855  uniioombllem6  25856  opnmbllem  25869  volcn  25874  i1fadd  25963  itg1addlem2  25965  i1fres  25973  itgle  26077  itgsplitioo  26105  ellimc3  26146  limcflflem  26147  limcflf  26148  limcmo  26149  limcres  26153  limciun  26161  perfdvf  26170  dvidlem  26182  dvnres  26198  dvlipcn  26261  dv11cn  26268  lhop2  26282  dvcnvrelem2  26285  tdeglem4  26325  plysub  26485  coeeulem  26490  plydiveu  26568  vieta1lem2  26583  plyexmo  26585  aaliou2b  26617  taylfval  26635  psercn  26702  pserdvlem2  26704  pserdv  26705  logdivlti  26897  efopnlem2  26934  acoscos  27170  xrlimcnp  27245  efrlim  27246  lgamucov  27314  basellem9  27365  perfectlem1  27505  perfectlem2  27506  lgsqrlem4  27625  gausslemma2dlem4  27645  lgsquad2lem1  27660  lgsquad2lem2  27661  dchrisum0lem1  27792  pntlem3  27885  pntleml  27887  qrngdiv  27900  nosupbday  27981  noinfbday  27996  noetainflem4  28016  madebdaylemlrcut  28204  oniso  28576  pw2divscan4d  28749  bdayfinbndlem1  28772  ttgcontlem1  29381  brbtwn2  29402  colinearalglem4  29406  ax5seglem1  29425  axcontlem4  29464  axcontlem7  29467  wlkp1lem3  30173  wlkp1lem7  30177  wlkp1lem8  30178  pthdlem1  30271  conngrv2edg  30715  mptiffisupp  33205  0mplrim  34065  psrgsum  34099  esplyfv1  34120  esplyfv  34121  esplyfval3  34123  txomap  34385  rmulccn  34479  cvxpconn  35922  cvxsconn  35923  cvmlift2lem10  35992  knoppcnlem10  37284  itg2gt0cn  38507  resubeqsub  43403  flt4lem7  43603  nna4b4nsq  43604  omabs2  44271  nadd2rabex  44325  enrelmap  44935  k0004lem3  45087  sineq0ALT  45857  xlimconst  46751  evenwodadd  47827  cjnpoly  47855  2ltceilhalf  48318  2timesltsqm1  48365  odz2prm2pw  48564  fmtno4prmfac  48573  lighneallem3  48608  lighneallem4a  48609  lighneallem4  48611  gpg3kgrtriexlem3  49099  fllog2  49596  2arymptfv  49678  prelrrx2b  49742  rrxsphere  49776  2sphere  49777  line2  49780  line2x  49782  line2y  49783