Theorem mp3an2i 1468

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  onnseq  8316  oeoalem  8563  oeoelem  8565  domssex2  9107  domssex  9108  dif1enOLD  9132  sniffsupp  9358  cantnfp1lem1  9638  en2eleq  9968  en2other2  9969  infxpenc  9978  infxpenc2lem1  9979  mappwen  10072  dfac12lem2  10105  ackbij1b  10198  fin23lem26  10285  ttukeylem5  10473  gchac  10641  wunex2  10698  00id  11356  nngt1ne1  12222  gtndiv  12618  nn01to3  12907  rpnnen1lem2  12943  nnledivrp  13072  xrre3  13138  max0sub  13163  xsubge0  13228  xrub  13279  bernneq  14201  faclbnd6  14271  bc0k  14283  brfi1indALT  14482  wrdlen2i  14915  01sqrexlem5  15219  01sqrexlem7  15221  sqreulem  15333  0.999...  15854  bpoly3  16031  fsumcube  16033  cos2t  16153  cos2tsin  16154  sin01gt0  16165  cos01gt0  16166  absefib  16173  efieq1re  16174  3dvds  16308  nno  16359  gcdcllem3  16478  gcdn0gt0  16495  divgcdodd  16687  pythagtriplem4  16797  pythagtriplem11  16803  pythagtriplem12  16804  pythagtriplem13  16805  pythagtriplem14  16806  pcfac  16877  prmreclem1  16894  vdwlem12  16970  ramval  16986  ramub2  16992  prmolelcmf  17026  prmgaplcmlem2  17030  firest  17402  yonffthlem  18250  gsumval2a  18619  prdsinvlem  18988  f1otrspeq  19384  pmtrf  19392  pmtrmvd  19393  pmtrfinv  19398  gexex  19790  cnaddinv  19808  prdsmgp  20067  zringlpirlem1  21379  zringinvg  21382  pzriprnglem10  21407  frgpcyg  21490  redvr  21533  frlmphllem  21696  frlmup4  21717  evls1val  22214  evls1sca  22217  smadiadetlem1  22556  smadiadetlem3lem0  22559  smadiadet  22564  d0mat2pmat  22632  chpmat0d  22728  neiptoptop  23025  upxp  23517  uptx  23519  pt1hmeo  23700  tgpconncompeqg  24006  qustgplem  24015  cnextucn  24197  psmetge0  24207  xmetge0  24239  xbln0  24309  tmsxpsval2  24434  metustid  24449  icopnfcld  24662  iocmnfcld  24663  ioo2blex  24689  tgioo  24691  blcvx  24693  xrsmopn  24708  recld2  24710  metdcn2  24735  cnmptre  24828  icchmeo  24845  icchmeoOLD  24846  cnheiborlem  24860  cnheibor  24861  lebnumii  24872  phtpyco2  24896  pi1xfrf  24960  pi1xfr  24962  pi1xfrcnvlem  24963  pi1xfrcnv  24964  pi1coghm  24968  ehleudisval  25326  ovolmge0  25385  ovolctb2  25400  nulmbl2  25444  unmbl  25445  ioombl1lem4  25469  ovolioo  25476  uniioombllem2  25491  uniioombllem4  25494  uniioombllem5  25495  uniioombllem6  25496  opnmbllem  25509  volcn  25514  i1fadd  25603  itg1addlem2  25605  i1fres  25613  itgle  25718  itgsplitioo  25746  ellimc3  25787  limcflflem  25788  limcflf  25789  limcmo  25790  limcres  25794  limciun  25802  perfdvf  25811  dvidlem  25823  dvnres  25840  dvlipcn  25906  dv11cn  25913  lhop2  25927  dvcnvrelem2  25930  tdeglem4  25972  plysub  26131  coeeulem  26136  plydiveu  26213  vieta1lem2  26226  plyexmo  26228  aaliou2b  26256  taylfval  26273  psercn  26343  pserdvlem2  26345  pserdv  26346  logdivlti  26536  efopnlem2  26573  acoscos  26810  xrlimcnp  26885  efrlim  26886  efrlimOLD  26887  lgamucov  26955  basellem9  27006  perfectlem1  27147  perfectlem2  27148  lgsqrlem4  27267  gausslemma2dlem4  27287  lgsquad2lem1  27302  lgsquad2lem2  27303  dchrisum0lem1  27434  pntlem3  27527  pntleml  27529  qrngdiv  27542  nosupbday  27624  noinfbday  27639  noetainflem4  27659  madebdaylemlrcut  27817  onsiso  28176  ttgcontlem1  28819  brbtwn2  28839  colinearalglem4  28843  ax5seglem1  28862  axcontlem4  28901  axcontlem7  28904  wlkp1lem3  29610  wlkp1lem7  29614  wlkp1lem8  29615  pthdlem1  29703  conngrv2edg  30131  mptiffisupp  32623  elringlsm  33371  txomap  33831  rmulccn  33925  revpfxsfxrev  35110  cvxpconn  35236  cvxsconn  35237  cvmlift2lem10  35306  knoppcnlem10  36497  itg2gt0cn  37676  resubeqsub  42425  flt4lem7  42654  nna4b4nsq  42655  omabs2  43328  nadd2rabex  43382  enrelmap  43993  k0004lem3  44145  sineq0ALT  44933  xlimconst  45830  2ltceilhalf  47333  odz2prm2pw  47568  fmtno4prmfac  47577  lighneallem3  47612  lighneallem4a  47613  lighneallem4  47615  gpg3kgrtriexlem3  48080  fllog2  48561  2arymptfv  48643  prelrrx2b  48707  rrxsphere  48741  2sphere  48742  line2  48745  line2x  48747  line2y  48748