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  8264  oeoalem  8511  oeoelem  8513  domssex2  9050  domssex  9051  sniffsupp  9284  cantnfp1lem1  9568  en2eleq  9899  en2other2  9900  infxpenc  9909  infxpenc2lem1  9910  mappwen  10003  dfac12lem2  10036  ackbij1b  10129  fin23lem26  10216  ttukeylem5  10404  gchac  10572  wunex2  10629  00id  11288  nngt1ne1  12154  gtndiv  12550  nn01to3  12839  rpnnen1lem2  12875  nnledivrp  13004  xrre3  13070  max0sub  13095  xsubge0  13160  xrub  13211  bernneq  14136  faclbnd6  14206  bc0k  14218  brfi1indALT  14417  wrdlen2i  14849  01sqrexlem5  15153  01sqrexlem7  15155  sqreulem  15267  0.999...  15788  bpoly3  15965  fsumcube  15967  cos2t  16087  cos2tsin  16088  sin01gt0  16099  cos01gt0  16100  absefib  16107  efieq1re  16108  3dvds  16242  nno  16293  gcdcllem3  16412  gcdn0gt0  16429  divgcdodd  16621  pythagtriplem4  16731  pythagtriplem11  16737  pythagtriplem12  16738  pythagtriplem13  16739  pythagtriplem14  16740  pcfac  16811  prmreclem1  16828  vdwlem12  16904  ramval  16920  ramub2  16926  prmolelcmf  16960  prmgaplcmlem2  16964  firest  17336  yonffthlem  18188  gsumval2a  18593  prdsinvlem  18962  f1otrspeq  19359  pmtrf  19367  pmtrmvd  19368  pmtrfinv  19373  gexex  19765  cnaddinv  19783  prdsmgp  20069  zringlpirlem1  21399  zringinvg  21402  pzriprnglem10  21427  frgpcyg  21510  redvr  21554  frlmphllem  21717  frlmup4  21738  evls1val  22235  evls1sca  22238  smadiadetlem1  22577  smadiadetlem3lem0  22580  smadiadet  22585  d0mat2pmat  22653  chpmat0d  22749  neiptoptop  23046  upxp  23538  uptx  23540  pt1hmeo  23721  tgpconncompeqg  24027  qustgplem  24036  cnextucn  24217  psmetge0  24227  xmetge0  24259  xbln0  24329  tmsxpsval2  24454  metustid  24469  icopnfcld  24682  iocmnfcld  24683  ioo2blex  24709  tgioo  24711  blcvx  24713  xrsmopn  24728  recld2  24730  metdcn2  24755  cnmptre  24848  icchmeo  24865  icchmeoOLD  24866  cnheiborlem  24880  cnheibor  24881  lebnumii  24892  phtpyco2  24916  pi1xfrf  24980  pi1xfr  24982  pi1xfrcnvlem  24983  pi1xfrcnv  24984  pi1coghm  24988  ehleudisval  25346  ovolmge0  25405  ovolctb2  25420  nulmbl2  25464  unmbl  25465  ioombl1lem4  25489  ovolioo  25496  uniioombllem2  25511  uniioombllem4  25514  uniioombllem5  25515  uniioombllem6  25516  opnmbllem  25529  volcn  25534  i1fadd  25623  itg1addlem2  25625  i1fres  25633  itgle  25738  itgsplitioo  25766  ellimc3  25807  limcflflem  25808  limcflf  25809  limcmo  25810  limcres  25814  limciun  25822  perfdvf  25831  dvidlem  25843  dvnres  25860  dvlipcn  25926  dv11cn  25933  lhop2  25947  dvcnvrelem2  25950  tdeglem4  25992  plysub  26151  coeeulem  26156  plydiveu  26233  vieta1lem2  26246  plyexmo  26248  aaliou2b  26276  taylfval  26293  psercn  26363  pserdvlem2  26365  pserdv  26366  logdivlti  26556  efopnlem2  26593  acoscos  26830  xrlimcnp  26905  efrlim  26906  efrlimOLD  26907  lgamucov  26975  basellem9  27026  perfectlem1  27167  perfectlem2  27168  lgsqrlem4  27287  gausslemma2dlem4  27307  lgsquad2lem1  27322  lgsquad2lem2  27323  dchrisum0lem1  27454  pntlem3  27547  pntleml  27549  qrngdiv  27562  nosupbday  27644  noinfbday  27659  noetainflem4  27679  madebdaylemlrcut  27844  onsiso  28205  pw2divscan4d  28367  ttgcontlem1  28863  brbtwn2  28883  colinearalglem4  28887  ax5seglem1  28906  axcontlem4  28945  axcontlem7  28948  wlkp1lem3  29652  wlkp1lem7  29656  wlkp1lem8  29657  pthdlem1  29744  conngrv2edg  30175  mptiffisupp  32674  elringlsm  33358  esplyfv1  33590  esplyfv  33591  txomap  33847  rmulccn  33941  revpfxsfxrev  35160  cvxpconn  35286  cvxsconn  35287  cvmlift2lem10  35356  knoppcnlem10  36546  itg2gt0cn  37714  resubeqsub  42522  flt4lem7  42751  nna4b4nsq  42752  omabs2  43424  nadd2rabex  43478  enrelmap  44089  k0004lem3  44241  sineq0ALT  45028  xlimconst  45922  2ltceilhalf  47427  odz2prm2pw  47662  fmtno4prmfac  47671  lighneallem3  47706  lighneallem4a  47707  lighneallem4  47709  gpg3kgrtriexlem3  48184  fllog2  48668  2arymptfv  48750  prelrrx2b  48814  rrxsphere  48848  2sphere  48849  line2  48852  line2x  48854  line2y  48855