Theorem mp3an2i 1462

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  wfrlem17  7971  onnseq  7981  oeoalem  8222  oeoelem  8224  domssex2  8677  domssex  8678  sniffsupp  8873  cantnfp1lem1  9141  en2eleq  9434  en2other2  9435  infxpenc  9444  infxpenc2lem1  9445  mappwen  9538  dfac12lem2  9570  ackbij1b  9661  fin23lem26  9747  ttukeylem5  9935  gchac  10103  wunex2  10160  00id  10815  fiminreOLD  11590  nngt1ne1  11667  gtndiv  12060  nn01to3  12342  rpnnen1lem2  12377  nnledivrp  12502  xrre3  12565  max0sub  12590  xsubge0  12655  xrub  12706  bernneq  13591  faclbnd6  13660  bc0k  13672  wrdlen2i  14304  sqrlem5  14606  sqrlem7  14608  sqreulem  14719  0.999...  15237  bpoly3  15412  fsumcube  15414  cos2t  15531  cos2tsin  15532  sin01gt0  15543  cos01gt0  15544  absefib  15551  efieq1re  15552  3dvds  15680  nno  15733  gcdcllem3  15850  gcdn0gt0  15866  divgcdodd  16054  pythagtriplem4  16156  pythagtriplem11  16162  pythagtriplem12  16163  pythagtriplem13  16164  pythagtriplem14  16165  pcfac  16235  prmreclem1  16252  vdwlem12  16328  ramval  16344  ramub2  16350  prmolelcmf  16384  prmgaplcmlem2  16388  firest  16706  yonffthlem  17532  gsumval2a  17895  prdsinvlem  18208  f1otrspeq  18575  pmtrf  18583  pmtrmvd  18584  pmtrfinv  18589  gexex  18973  cnaddinv  18991  prdsmgp  19360  opsrtoslem2  20265  evls1val  20483  evls1sca  20486  zringlpirlem1  20631  zringinvg  20634  frgpcyg  20720  redvr  20761  frlmphllem  20924  frlmup4  20945  smadiadetlem1  21271  smadiadetlem3lem0  21274  smadiadet  21279  d0mat2pmat  21346  chpmat0d  21442  neiptoptop  21739  upxp  22231  uptx  22233  pt1hmeo  22414  tgpconncompeqg  22720  qustgplem  22729  cnextucn  22912  psmetge0  22922  xmetge0  22954  xbln0  23024  tmsxpsval2  23149  metustid  23164  icopnfcld  23376  iocmnfcld  23377  ioo2blex  23402  tgioo  23404  blcvx  23406  xrsmopn  23420  recld2  23422  metdcn2  23447  cnmptre  23531  icchmeo  23545  cnheiborlem  23558  cnheibor  23559  lebnumii  23570  phtpyco2  23594  pi1xfrf  23657  pi1xfr  23659  pi1xfrcnvlem  23660  pi1xfrcnv  23661  pi1coghm  23665  ehleudisval  24022  ovolmge0  24078  ovolctb2  24093  nulmbl2  24137  unmbl  24138  ioombl1lem4  24162  ovolioo  24169  uniioombllem2  24184  uniioombllem4  24187  uniioombllem5  24188  uniioombllem6  24189  opnmbllem  24202  volcn  24207  i1fadd  24296  itg1addlem2  24298  i1fres  24306  itgle  24410  itgsplitioo  24438  ellimc3  24477  limcflflem  24478  limcflf  24479  limcmo  24480  limcres  24484  limciun  24492  perfdvf  24501  dvidlem  24513  dvnres  24528  dvlipcn  24591  dv11cn  24598  lhop2  24612  dvcnvrelem2  24615  plysub  24809  coeeulem  24814  plydiveu  24887  vieta1lem2  24900  plyexmo  24902  aaliou2b  24930  taylfval  24947  psercn  25014  pserdvlem2  25016  pserdv  25017  logdivlti  25203  efopnlem2  25240  acoscos  25471  xrlimcnp  25546  efrlim  25547  lgamucov  25615  basellem9  25666  perfectlem1  25805  perfectlem2  25806  lgsqrlem4  25925  gausslemma2dlem4  25945  lgsquad2lem1  25960  lgsquad2lem2  25961  dchrisum0lem1  26092  pntlem3  26185  pntleml  26187  qrngdiv  26200  ttgcontlem1  26671  brbtwn2  26691  colinearalglem4  26695  ax5seglem1  26714  axcontlem4  26753  axcontlem7  26756  wlkp1lem3  27457  wlkp1lem7  27461  wlkp1lem8  27462  pthdlem1  27547  conngrv2edg  27974  txomap  31098  revpfxsfxrev  32362  cvmlift2lem10  32559  nosupbday  33205  itg2gt0cn  34962  enrelmap  40392  k0004lem3  40548  sineq0ALT  41320  xlimconst  42155  odz2prm2pw  43774  fmtno4prmfac  43783  lighneallem3  43821  lighneallem4a  43822  lighneallem4  43824  fllog2  44677  prelrrx2b  44750  rrxsphere  44784  2sphere  44785  line2  44788  line2x  44790  line2y  44791