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 583	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 207  df-an 396  df-3an 1089

This theorem is referenced by:  wfrlem17OLD  8381  onnseq  8400  oeoalem  8652  oeoelem  8654  domssex2  9203  domssex  9204  dif1enOLD  9228  sniffsupp  9469  cantnfp1lem1  9747  en2eleq  10077  en2other2  10078  infxpenc  10087  infxpenc2lem1  10088  mappwen  10181  dfac12lem2  10214  ackbij1b  10307  fin23lem26  10394  ttukeylem5  10582  gchac  10750  wunex2  10807  00id  11465  nngt1ne1  12322  gtndiv  12720  nn01to3  13006  rpnnen1lem2  13042  nnledivrp  13169  xrre3  13233  max0sub  13258  xsubge0  13323  xrub  13374  bernneq  14278  faclbnd6  14348  bc0k  14360  brfi1indALT  14559  wrdlen2i  14991  01sqrexlem5  15295  01sqrexlem7  15297  sqreulem  15408  0.999...  15929  bpoly3  16106  fsumcube  16108  cos2t  16226  cos2tsin  16227  sin01gt0  16238  cos01gt0  16239  absefib  16246  efieq1re  16247  3dvds  16379  nno  16430  gcdcllem3  16547  gcdn0gt0  16564  divgcdodd  16757  pythagtriplem4  16866  pythagtriplem11  16872  pythagtriplem12  16873  pythagtriplem13  16874  pythagtriplem14  16875  pcfac  16946  prmreclem1  16963  vdwlem12  17039  ramval  17055  ramub2  17061  prmolelcmf  17095  prmgaplcmlem2  17099  firest  17492  yonffthlem  18352  gsumval2a  18723  prdsinvlem  19089  f1otrspeq  19489  pmtrf  19497  pmtrmvd  19498  pmtrfinv  19503  gexex  19895  cnaddinv  19913  prdsmgp  20178  zringlpirlem1  21496  zringinvg  21499  pzriprnglem10  21524  frgpcyg  21615  redvr  21658  frlmphllem  21823  frlmup4  21844  evls1val  22345  evls1sca  22348  smadiadetlem1  22689  smadiadetlem3lem0  22692  smadiadet  22697  d0mat2pmat  22765  chpmat0d  22861  neiptoptop  23160  upxp  23652  uptx  23654  pt1hmeo  23835  tgpconncompeqg  24141  qustgplem  24150  cnextucn  24333  psmetge0  24343  xmetge0  24375  xbln0  24445  tmsxpsval2  24573  metustid  24588  icopnfcld  24809  iocmnfcld  24810  ioo2blex  24835  tgioo  24837  blcvx  24839  xrsmopn  24853  recld2  24855  metdcn2  24880  cnmptre  24973  icchmeo  24990  icchmeoOLD  24991  cnheiborlem  25005  cnheibor  25006  lebnumii  25017  phtpyco2  25041  pi1xfrf  25105  pi1xfr  25107  pi1xfrcnvlem  25108  pi1xfrcnv  25109  pi1coghm  25113  ehleudisval  25472  ovolmge0  25531  ovolctb2  25546  nulmbl2  25590  unmbl  25591  ioombl1lem4  25615  ovolioo  25622  uniioombllem2  25637  uniioombllem4  25640  uniioombllem5  25641  uniioombllem6  25642  opnmbllem  25655  volcn  25660  i1fadd  25749  itg1addlem2  25751  i1fres  25760  itgle  25865  itgsplitioo  25893  ellimc3  25934  limcflflem  25935  limcflf  25936  limcmo  25937  limcres  25941  limciun  25949  perfdvf  25958  dvidlem  25970  dvnres  25987  dvlipcn  26053  dv11cn  26060  lhop2  26074  dvcnvrelem2  26077  tdeglem4  26119  plysub  26278  coeeulem  26283  plydiveu  26358  vieta1lem2  26371  plyexmo  26373  aaliou2b  26401  taylfval  26418  psercn  26488  pserdvlem2  26490  pserdv  26491  logdivlti  26680  efopnlem2  26717  acoscos  26954  xrlimcnp  27029  efrlim  27030  efrlimOLD  27031  lgamucov  27099  basellem9  27150  perfectlem1  27291  perfectlem2  27292  lgsqrlem4  27411  gausslemma2dlem4  27431  lgsquad2lem1  27446  lgsquad2lem2  27447  dchrisum0lem1  27578  pntlem3  27671  pntleml  27673  qrngdiv  27686  nosupbday  27768  noinfbday  27783  noetainflem4  27803  madebdaylemlrcut  27955  ttgcontlem1  28917  brbtwn2  28938  colinearalglem4  28942  ax5seglem1  28961  axcontlem4  29000  axcontlem7  29003  wlkp1lem3  29711  wlkp1lem7  29715  wlkp1lem8  29716  pthdlem1  29802  conngrv2edg  30227  mptiffisupp  32705  elringlsm  33386  txomap  33780  rmulccn  33874  revpfxsfxrev  35083  cvxpconn  35210  cvxsconn  35211  cvmlift2lem10  35280  knoppcnlem10  36468  itg2gt0cn  37635  resubeqsub  42405  flt4lem7  42614  nna4b4nsq  42615  omabs2  43294  nadd2rabex  43348  enrelmap  43959  k0004lem3  44111  sineq0ALT  44908  xlimconst  45746  odz2prm2pw  47437  fmtno4prmfac  47446  lighneallem3  47481  lighneallem4a  47482  lighneallem4  47484  fllog2  48302  2arymptfv  48384  prelrrx2b  48448  rrxsphere  48482  2sphere  48483  line2  48486  line2x  48488  line2y  48489