Theorem mp3an2i 1464

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  wfrlem17OLD  8327  onnseq  8346  oeoalem  8598  oeoelem  8600  domssex2  9139  domssex  9140  dif1enOLD  9164  sniffsupp  9397  cantnfp1lem1  9675  en2eleq  10005  en2other2  10006  infxpenc  10015  infxpenc2lem1  10016  mappwen  10109  dfac12lem2  10141  ackbij1b  10236  fin23lem26  10322  ttukeylem5  10510  gchac  10678  wunex2  10735  00id  11393  nngt1ne1  12245  gtndiv  12643  nn01to3  12929  rpnnen1lem2  12965  nnledivrp  13090  xrre3  13154  max0sub  13179  xsubge0  13244  xrub  13295  bernneq  14196  faclbnd6  14263  bc0k  14275  brfi1indALT  14465  wrdlen2i  14897  01sqrexlem5  15197  01sqrexlem7  15199  sqreulem  15310  0.999...  15831  bpoly3  16006  fsumcube  16008  cos2t  16125  cos2tsin  16126  sin01gt0  16137  cos01gt0  16138  absefib  16145  efieq1re  16146  3dvds  16278  nno  16329  gcdcllem3  16446  gcdn0gt0  16463  divgcdodd  16651  pythagtriplem4  16756  pythagtriplem11  16762  pythagtriplem12  16763  pythagtriplem13  16764  pythagtriplem14  16765  pcfac  16836  prmreclem1  16853  vdwlem12  16929  ramval  16945  ramub2  16951  prmolelcmf  16985  prmgaplcmlem2  16989  firest  17382  yonffthlem  18239  gsumval2a  18610  prdsinvlem  18968  f1otrspeq  19356  pmtrf  19364  pmtrmvd  19365  pmtrfinv  19370  gexex  19762  cnaddinv  19780  prdsmgp  20045  zringlpirlem1  21233  zringinvg  21236  pzriprnglem10  21259  frgpcyg  21348  redvr  21389  frlmphllem  21554  frlmup4  21575  evls1val  22059  evls1sca  22062  smadiadetlem1  22384  smadiadetlem3lem0  22387  smadiadet  22392  d0mat2pmat  22460  chpmat0d  22556  neiptoptop  22855  upxp  23347  uptx  23349  pt1hmeo  23530  tgpconncompeqg  23836  qustgplem  23845  cnextucn  24028  psmetge0  24038  xmetge0  24070  xbln0  24140  tmsxpsval2  24268  metustid  24283  icopnfcld  24504  iocmnfcld  24505  ioo2blex  24530  tgioo  24532  blcvx  24534  xrsmopn  24548  recld2  24550  metdcn2  24575  cnmptre  24668  icchmeo  24685  icchmeoOLD  24686  cnheiborlem  24700  cnheibor  24701  lebnumii  24712  phtpyco2  24736  pi1xfrf  24800  pi1xfr  24802  pi1xfrcnvlem  24803  pi1xfrcnv  24804  pi1coghm  24808  ehleudisval  25167  ovolmge0  25226  ovolctb2  25241  nulmbl2  25285  unmbl  25286  ioombl1lem4  25310  ovolioo  25317  uniioombllem2  25332  uniioombllem4  25335  uniioombllem5  25336  uniioombllem6  25337  opnmbllem  25350  volcn  25355  i1fadd  25444  itg1addlem2  25446  i1fres  25455  itgle  25559  itgsplitioo  25587  ellimc3  25628  limcflflem  25629  limcflf  25630  limcmo  25631  limcres  25635  limciun  25643  perfdvf  25652  dvidlem  25664  dvnres  25681  dvlipcn  25746  dv11cn  25753  lhop2  25767  dvcnvrelem2  25770  tdeglem4  25812  plysub  25968  coeeulem  25973  plydiveu  26047  vieta1lem2  26060  plyexmo  26062  aaliou2b  26090  taylfval  26107  psercn  26174  pserdvlem2  26176  pserdv  26177  logdivlti  26364  efopnlem2  26401  acoscos  26634  xrlimcnp  26709  efrlim  26710  lgamucov  26778  basellem9  26829  perfectlem1  26968  perfectlem2  26969  lgsqrlem4  27088  gausslemma2dlem4  27108  lgsquad2lem1  27123  lgsquad2lem2  27124  dchrisum0lem1  27255  pntlem3  27348  pntleml  27350  qrngdiv  27363  nosupbday  27444  noinfbday  27459  noetainflem4  27479  madebdaylemlrcut  27630  ttgcontlem1  28409  brbtwn2  28430  colinearalglem4  28434  ax5seglem1  28453  axcontlem4  28492  axcontlem7  28495  wlkp1lem3  29199  wlkp1lem7  29203  wlkp1lem8  29204  pthdlem1  29290  conngrv2edg  29715  mptiffisupp  32182  elringlsm  32777  txomap  33112  revpfxsfxrev  34404  cvmlift2lem10  34601  gg-rmulccn  35465  itg2gt0cn  36846  resubeqsub  41604  flt4lem7  41703  nna4b4nsq  41704  omabs2  42384  nadd2rabex  42438  enrelmap  43050  k0004lem3  43202  sineq0ALT  44000  xlimconst  44839  odz2prm2pw  46529  fmtno4prmfac  46538  lighneallem3  46573  lighneallem4a  46574  lighneallem4  46576  fllog2  47341  2arymptfv  47423  prelrrx2b  47487  rrxsphere  47521  2sphere  47522  line2  47525  line2x  47527  line2y  47528