Theorem mp3an2i 1496

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  onnseq  8377  oeoalem  8630  oeoelem  8632  domssex2  9181  domssex  9182  sniffsupp  9416  cantnfp1lem1  9703  en2eleq  10111  en2other2  10112  infxpenc  10121  infxpenc2lem1  10122  mappwen  10215  dfac12lem2  10247  ackbij1b  10340  fin23lem26  10427  ttukeylem5  10615  gchac  10790  wunex2  10847  00id  11509  nngt1ne1  12391  gtndiv  12800  nn01to3  13092  rpnnen1lem2  13129  nnledivrp  13258  xrre3  13325  max0sub  13350  xsubge0  13415  xrub  13466  bernneq  14397  faclbnd6  14467  bc0k  14479  brfi1indALT  14679  revpfxsfxrev  14942  wrdlen2i  15119  01sqrexlem5  15439  01sqrexlem7  15441  sqreulem  15553  0.999...  16076  bpoly3  16250  fsumcube  16252  cos2t  16372  cos2tsin  16373  sin01gt0  16384  cos01gt0  16385  absefib  16392  efieq1re  16393  3dvds  16527  nno  16578  gcdcllem3  16697  gcdn0gt0  16716  divgcdodd  16912  pythagtriplem4  17023  pythagtriplem11  17029  pythagtriplem12  17030  pythagtriplem13  17031  pythagtriplem14  17032  pcfac  17103  prmreclem1  17120  vdwlem12  17196  ramval  17212  ramub2  17218  prmolelcmf  17252  prmgaplcmlem2  17256  firest  17629  yonffthlem  18482  gsumval2a  18900  prdsinvlem  19285  f1otrspeq  19688  pmtrf  19696  pmtrmvd  19697  pmtrfinv  19702  gexex  20094  cnaddinv  20112  prdsmgp  20398  elmgplsm  20399  zringlpirlem1  21795  zringinvg  21798  pzriprnglem10  21823  frgpcyg  21906  redvr  21950  frlmphllem  22113  frlmup4  22134  evls1val  22665  evls1sca  22668  smadiadetlem1  23004  smadiadetlem3lem0  23007  smadiadet  23012  d0mat2pmat  23083  chpmat0d  23179  neiptoptop  23476  upxp  23969  uptx  23971  pt1hmeo  24152  tgpconncompeqg  24458  qustgplem  24467  cnextucn  24648  psmetge0  24658  xmetge0  24690  xbln0  24760  tmsxpsval2  24885  metustid  24900  icopnfcld  25113  iocmnfcld  25114  ioo2blex  25140  tgioo  25142  blcvx  25144  xrsmopn  25159  recld2  25161  metdcn2  25186  cnmptre  25275  icchmeo  25289  cnheiborlem  25302  cnheibor  25303  lebnumii  25314  phtpyco2  25338  pi1xfrf  25401  pi1xfr  25403  pi1xfrcnvlem  25404  pi1xfrcnv  25405  pi1coghm  25409  ehleudisval  25767  ovolmge0  25825  ovolctb2  25840  nulmbl2  25884  unmbl  25885  ioombl1lem4  25909  ovolioo  25916  uniioombllem2  25931  uniioombllem4  25934  uniioombllem5  25935  uniioombllem6  25936  opnmbllem  25949  volcn  25954  i1fadd  26043  itg1addlem2  26045  i1fres  26053  itgle  26157  itgsplitioo  26185  ellimc3  26226  limcflflem  26227  limcflf  26228  limcmo  26229  limcres  26233  limciun  26241  perfdvf  26250  dvidlem  26262  dvnres  26278  dvlipcn  26341  dv11cn  26348  lhop2  26362  dvcnvrelem2  26365  tdeglem4  26405  plysub  26565  coeeulem  26570  plydiveu  26646  vieta1lem2  26661  plyexmo  26663  aaliou2b  26695  taylfval  26713  psercn  26780  pserdvlem2  26782  pserdv  26783  logdivlti  26975  efopnlem2  27012  acoscos  27248  xrlimcnp  27323  efrlim  27324  lgamucov  27392  basellem9  27443  perfectlem1  27583  perfectlem2  27584  lgsqrlem4  27703  gausslemma2dlem4  27723  lgsquad2lem1  27738  lgsquad2lem2  27739  dchrisum0lem1  27870  pntlem3  27963  pntleml  27965  qrngdiv  27978  flt4lem7  28016  nosupbday  28089  noinfbday  28104  noetainflem4  28124  madebdaylemlrcut  28312  oniso  28684  pw2divscan4d  28857  bdayfinbndlem1  28880  ttgcontlem1  29489  brbtwn2  29510  colinearalglem4  29514  ax5seglem1  29533  axcontlem4  29572  axcontlem7  29575  wlkp1lem3  30281  wlkp1lem7  30285  wlkp1lem8  30286  pthdlem1  30379  conngrv2edg  30823  mptiffisupp  33354  0mplrim  34213  psrgsum  34247  esplyfv1  34268  esplyfv  34269  esplyfval3  34271  txomap  34533  rmulccn  34627  omssubadd  34999  weexenwe  35847  jltalephlem  36024  cvxpconn  36173  cvxsconn  36174  cvmlift2lem10  36243  knoppcnlem10  37545  pibt2  38531  itg2gt0cn  38784  resubeqsub  43672  omabs2  44524  nadd2rabex  44578  enrelmap  45187  k0004lem3  45339  sineq0ALT  46108  mpoexwd  46116  grpcanonhfstruct  46228  xlimconst  47038  evenwodadd  48114  cjnpoly  48142  2ltceilhalf  48605  2timesltsqm1  48652  odz2prm2pw  48851  fmtno4prmfac  48860  lighneallem3  48895  lighneallem4a  48896  lighneallem4  48898  gpg3kgrtriexlem3  49386  fllog2  49883  2arymptfv  49965  rrxsphere  50063  2sphere  50064  line2  50067