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  8340  oeoalem  8591  oeoelem  8593  domssex2  9135  domssex  9136  sniffsupp  9370  cantnfp1lem1  9657  en2eleq  10011  en2other2  10012  infxpenc  10021  infxpenc2lem1  10022  mappwen  10115  dfac12lem2  10147  ackbij1b  10240  fin23lem26  10327  ttukeylem5  10515  gchac  10684  wunex2  10741  00id  11403  nngt1ne1  12283  gtndiv  12691  nn01to3  12983  rpnnen1lem2  13019  nnledivrp  13148  xrre3  13215  max0sub  13240  xsubge0  13305  xrub  13356  bernneq  14285  faclbnd6  14355  bc0k  14367  brfi1indALT  14567  revpfxsfxrev  14829  wrdlen2i  15005  01sqrexlem5  15323  01sqrexlem7  15325  sqreulem  15437  0.999...  15961  bpoly3  16137  fsumcube  16139  cos2t  16259  cos2tsin  16260  sin01gt0  16271  cos01gt0  16272  absefib  16279  efieq1re  16280  3dvds  16414  nno  16465  gcdcllem3  16584  gcdn0gt0  16601  divgcdodd  16794  pythagtriplem4  16904  pythagtriplem11  16910  pythagtriplem12  16911  pythagtriplem13  16912  pythagtriplem14  16913  pcfac  16984  prmreclem1  17001  vdwlem12  17077  ramval  17093  ramub2  17099  prmolelcmf  17133  prmgaplcmlem2  17137  firest  17510  yonffthlem  18363  gsumval2a  18768  prdsinvlem  19140  f1otrspeq  19542  pmtrf  19550  pmtrmvd  19551  pmtrfinv  19556  gexex  19948  cnaddinv  19966  prdsmgp  20252  elmgplsm  20253  zringlpirlem1  21642  zringinvg  21645  pzriprnglem10  21670  frgpcyg  21753  redvr  21797  frlmphllem  21960  frlmup4  21981  evls1val  22510  evls1sca  22513  smadiadetlem1  22849  smadiadetlem3lem0  22852  smadiadet  22857  d0mat2pmat  22925  chpmat0d  23021  neiptoptop  23318  upxp  23810  uptx  23812  pt1hmeo  23993  tgpconncompeqg  24299  qustgplem  24308  cnextucn  24489  psmetge0  24499  xmetge0  24531  xbln0  24601  tmsxpsval2  24726  metustid  24741  icopnfcld  24954  iocmnfcld  24955  ioo2blex  24981  tgioo  24983  blcvx  24985  xrsmopn  25000  recld2  25002  metdcn2  25027  cnmptre  25116  icchmeo  25130  cnheiborlem  25143  cnheibor  25144  lebnumii  25155  phtpyco2  25179  pi1xfrf  25242  pi1xfr  25244  pi1xfrcnvlem  25245  pi1xfrcnv  25246  pi1coghm  25250  ehleudisval  25608  ovolmge0  25666  ovolctb2  25681  nulmbl2  25725  unmbl  25726  ioombl1lem4  25750  ovolioo  25757  uniioombllem2  25772  uniioombllem4  25775  uniioombllem5  25776  uniioombllem6  25777  opnmbllem  25790  volcn  25795  i1fadd  25884  itg1addlem2  25886  i1fres  25894  itgle  25999  itgsplitioo  26027  ellimc3  26068  limcflflem  26069  limcflf  26070  limcmo  26071  limcres  26075  limciun  26083  perfdvf  26092  dvidlem  26104  dvnres  26120  dvlipcn  26183  dv11cn  26190  lhop2  26204  dvcnvrelem2  26207  tdeglem4  26247  plysub  26406  coeeulem  26411  plydiveu  26489  vieta1lem2  26502  plyexmo  26504  aaliou2b  26534  taylfval  26552  psercn  26619  pserdvlem2  26621  pserdv  26622  logdivlti  26815  efopnlem2  26852  acoscos  27088  xrlimcnp  27163  efrlim  27164  lgamucov  27232  basellem9  27283  perfectlem1  27423  perfectlem2  27424  lgsqrlem4  27543  gausslemma2dlem4  27563  lgsquad2lem1  27578  lgsquad2lem2  27579  dchrisum0lem1  27710  pntlem3  27803  pntleml  27805  qrngdiv  27818  nosupbday  27899  noinfbday  27914  noetainflem4  27934  madebdaylemlrcut  28122  oniso  28494  pw2divscan4d  28667  bdayfinbndlem1  28690  ttgcontlem1  29264  brbtwn2  29285  colinearalglem4  29289  ax5seglem1  29308  axcontlem4  29347  axcontlem7  29350  wlkp1lem3  30053  wlkp1lem7  30057  wlkp1lem8  30058  pthdlem1  30145  conngrv2edg  30576  mptiffisupp  33068  0mplrim  33928  psrgsum  33962  esplyfv1  33983  esplyfv  33984  esplyfval3  33986  txomap  34248  rmulccn  34342  cvxpconn  35747  cvxsconn  35748  cvmlift2lem10  35817  knoppcnlem10  37124  itg2gt0cn  38359  resubeqsub  43224  flt4lem7  43424  nna4b4nsq  43425  omabs2  44092  nadd2rabex  44146  enrelmap  44756  k0004lem3  44908  sineq0ALT  45678  xlimconst  46572  2ltceilhalf  48102  2timesltsqm1  48149  odz2prm2pw  48348  fmtno4prmfac  48357  lighneallem3  48392  lighneallem4a  48393  lighneallem4  48395  gpg3kgrtriexlem3  48883  fllog2  49381  2arymptfv  49463  prelrrx2b  49527  rrxsphere  49561  2sphere  49562  line2  49565  line2x  49567  line2y  49568