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  8336  oeoalem  8587  oeoelem  8589  domssex2  9138  domssex  9139  sniffsupp  9373  cantnfp1lem1  9660  en2eleq  10014  en2other2  10015  infxpenc  10024  infxpenc2lem1  10025  mappwen  10118  dfac12lem2  10150  ackbij1b  10243  fin23lem26  10330  ttukeylem5  10518  gchac  10693  wunex2  10750  00id  11412  nngt1ne1  12292  gtndiv  12701  nn01to3  12993  rpnnen1lem2  13029  nnledivrp  13158  xrre3  13225  max0sub  13250  xsubge0  13315  xrub  13366  bernneq  14295  faclbnd6  14365  bc0k  14377  brfi1indALT  14577  revpfxsfxrev  14839  wrdlen2i  15015  01sqrexlem5  15335  01sqrexlem7  15337  sqreulem  15449  0.999...  15972  bpoly3  16148  fsumcube  16150  cos2t  16270  cos2tsin  16271  sin01gt0  16282  cos01gt0  16283  absefib  16290  efieq1re  16291  3dvds  16425  nno  16476  gcdcllem3  16595  gcdn0gt0  16612  divgcdodd  16805  pythagtriplem4  16915  pythagtriplem11  16921  pythagtriplem12  16922  pythagtriplem13  16923  pythagtriplem14  16924  pcfac  16995  prmreclem1  17012  vdwlem12  17088  ramval  17104  ramub2  17110  prmolelcmf  17144  prmgaplcmlem2  17148  firest  17521  yonffthlem  18374  gsumval2a  18789  prdsinvlem  19173  f1otrspeq  19575  pmtrf  19583  pmtrmvd  19584  pmtrfinv  19589  gexex  19981  cnaddinv  19999  prdsmgp  20285  elmgplsm  20286  zringlpirlem1  21676  zringinvg  21679  pzriprnglem10  21704  frgpcyg  21787  redvr  21831  frlmphllem  21994  frlmup4  22015  evls1val  22546  evls1sca  22549  smadiadetlem1  22885  smadiadetlem3lem0  22888  smadiadet  22893  d0mat2pmat  22964  chpmat0d  23060  neiptoptop  23357  upxp  23850  uptx  23852  pt1hmeo  24033  tgpconncompeqg  24339  qustgplem  24348  cnextucn  24529  psmetge0  24539  xmetge0  24571  xbln0  24641  tmsxpsval2  24766  metustid  24781  icopnfcld  24994  iocmnfcld  24995  ioo2blex  25021  tgioo  25023  blcvx  25025  xrsmopn  25040  recld2  25042  metdcn2  25067  cnmptre  25156  icchmeo  25170  cnheiborlem  25183  cnheibor  25184  lebnumii  25195  phtpyco2  25219  pi1xfrf  25282  pi1xfr  25284  pi1xfrcnvlem  25285  pi1xfrcnv  25286  pi1coghm  25290  ehleudisval  25648  ovolmge0  25706  ovolctb2  25721  nulmbl2  25765  unmbl  25766  ioombl1lem4  25790  ovolioo  25797  uniioombllem2  25812  uniioombllem4  25815  uniioombllem5  25816  uniioombllem6  25817  opnmbllem  25830  volcn  25835  i1fadd  25924  itg1addlem2  25926  i1fres  25934  itgle  26039  itgsplitioo  26067  ellimc3  26108  limcflflem  26109  limcflf  26110  limcmo  26111  limcres  26115  limciun  26123  perfdvf  26132  dvidlem  26144  dvnres  26160  dvlipcn  26223  dv11cn  26230  lhop2  26244  dvcnvrelem2  26247  tdeglem4  26287  plysub  26446  coeeulem  26451  plydiveu  26529  vieta1lem2  26542  plyexmo  26544  aaliou2b  26574  taylfval  26592  psercn  26659  pserdvlem2  26661  pserdv  26662  logdivlti  26855  efopnlem2  26892  acoscos  27128  xrlimcnp  27203  efrlim  27204  lgamucov  27272  basellem9  27323  perfectlem1  27463  perfectlem2  27464  lgsqrlem4  27583  gausslemma2dlem4  27603  lgsquad2lem1  27618  lgsquad2lem2  27619  dchrisum0lem1  27750  pntlem3  27843  pntleml  27845  qrngdiv  27858  nosupbday  27939  noinfbday  27954  noetainflem4  27974  madebdaylemlrcut  28162  oniso  28534  pw2divscan4d  28707  bdayfinbndlem1  28730  ttgcontlem1  29327  brbtwn2  29348  colinearalglem4  29352  ax5seglem1  29371  axcontlem4  29410  axcontlem7  29413  wlkp1lem3  30119  wlkp1lem7  30123  wlkp1lem8  30124  pthdlem1  30217  conngrv2edg  30661  mptiffisupp  33152  0mplrim  34011  psrgsum  34045  esplyfv1  34066  esplyfv  34067  esplyfval3  34069  txomap  34331  rmulccn  34425  cvxpconn  35808  cvxsconn  35809  cvmlift2lem10  35878  knoppcnlem10  37186  itg2gt0cn  38411  resubeqsub  43292  flt4lem7  43492  nna4b4nsq  43493  omabs2  44160  nadd2rabex  44214  enrelmap  44824  k0004lem3  44976  sineq0ALT  45746  xlimconst  46640  evenwodadd  47716  cjnpoly  47744  2ltceilhalf  48207  2timesltsqm1  48254  odz2prm2pw  48453  fmtno4prmfac  48462  lighneallem3  48497  lighneallem4a  48498  lighneallem4  48500  gpg3kgrtriexlem3  48988  fllog2  49485  2arymptfv  49567  prelrrx2b  49631  rrxsphere  49665  2sphere  49666  line2  49669  line2x  49671  line2y  49672