Theorem simp2 1029

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 1025	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  simpl2  1032  simpr2  1035  simp2i  1038  simp2d  1041  simp12  1059  simp22  1062  simp32  1065  syld3an3  1323  3ianorr  1350  intn3an2d  1398  stoic4b  1482  nlim0  4537  tfisi  4732  sotri2  5183  sotri3  5184  feq123  5523  sefvex  5714  fvmptt  5794  fnfvima  5947  cocan1  5987  cocan2  5988  ovexg  6113  ovmpox  6211  ovmpoga  6212  fvmpopr2d  6219  caovimo  6277  suppval1  6473  suppimacnvfn  6480  suppfnss  6491  tfr1onlembxssdm  6608  tfr1onlembfn  6609  tfrcllembxssdm  6621  tfrcllembfn  6622  freccllem  6667  frecfcllem  6669  frecsuclem  6671  frecrdg  6673  domssr  7058  mapxpen  7142  dif1en  7177  diffifi  7192  unsnfidcex  7221  unfidisj  7223  undifdc  7225  resfnfinfinss  7247  funrnfi  7250  fissfi  7257  sbthlemi9  7276  elfir  7301  difinfsn  7434  ctssdc  7447  djuassen  7567  xpdjuen  7568  mulcanenq  7746  ltanqg  7761  mulcanenq0ec  7806  addnnnq0  7810  distrprg  7949  aptipr  8002  addsrpr  8106  mulsrpr  8107  mulasssrg  8119  ltpsrprg  8164  axmulass  8234  axpre-ltadd  8247  subadd2  8524  nppcan  8542  nppcan3  8544  subsub2  8548  subsub4  8553  npncan3  8558  pnpcan  8559  pnncan  8561  subcan  8575  ltadd1  8751  leadd1  8752  leadd2  8753  ltsubadd  8754  ltsubadd2  8755  lesubadd  8756  lesubadd2  8757  ltaddsub  8758  leaddsub  8760  lesub1  8778  lesub2  8779  ltsub1  8780  ltsub2  8781  gt0add  8895  apreap  8909  lemul1  8915  reapmul1lem  8916  reapmul1  8917  reapadd1  8918  remulext1  8921  remulext2  8922  apadd2  8931  mulext2  8935  mulap0r  8937  leltap  8947  ltap  8955  apsub1  8964  recexaplem2  8974  mulcanap  8987  mulcanap2  8988  divvalap  8998  divmulap  8999  divcanap1  9005  diveqap0  9006  divap0b  9007  divrecap  9012  divassap  9014  div23ap  9015  divdirap  9021  divcanap3  9022  div11ap  9024  diveqap1  9029  divmuldivap  9036  divcanap5  9038  redivclap  9055  div2negap  9059  apmul1  9112  apmul2  9113  div2subap  9161  ltdiv1  9192  ledivmul  9201  lemuldiv  9205  lt2msq1  9209  ltdiv23  9216  squeeze0  9228  ofnegsub  9286  zaddcllemneg  9666  zfidc  9706  eluzsub  9935  nn01to3  10000  rpgecl  10066  addlelt  10152  xleadd1  10260  xltadd1  10261  lbioog  10298  ubioc1  10314  ubicc2  10370  icoshftf1o  10376  fzen  10430  nelfzo  10542  ubmelfzo  10601  ssfzo12  10625  ubmelm1fzo  10627  fzosplitprm1  10636  zsupssdc  10656  rebtwn2zlemshrink  10671  qbtwnre  10674  icogelb  10683  flqwordi  10706  flqword2  10707  flltdivnn0lt  10722  modqcl  10746  mulqmod0  10750  modqmulnn  10762  modqabs2  10778  modqmuladdnn0  10788  qnegmod  10789  addmodid  10792  modqm1p1mod0  10795  modifeq2int  10806  modqdi  10812  modqeqmodmin  10814  modfzo0difsn  10815  frec2uzf1od  10826  exp3val  10961  expnegap0  10967  expgt1  10997  exprecap  11000  expmulzap  11005  leexp2a  11012  expubnd  11016  mulbinom2  11076  bernneq2  11082  expnbnd  11084  fihashss  11240  fihashssdif  11242  fimaxq  11253  ccatval2  11349  ccatass  11359  ccatw2s1leng  11389  ccat2s1fvwd  11398  swrdval  11403  swrdnd  11414  pfxfv  11439  pfxpfx  11463  ccats1pfxeq  11469  ccats1pfxeqrex  11470  s3cl  11541  s3fv0g  11546  s3fv1g  11547  s3fv2g  11548  shftuz  11565  shftfibg  11568  cjdivap  11658  resqrtcl  11778  absdivap  11819  abssubne0  11840  maxleast  11962  lemininf  11983  ltmininf  11984  xrmaxltsup  12007  xrmaxaddlem  12009  xrmaxadd  12010  xrmineqinf  12018  xrltmininf  12019  xrminltinf  12021  xrminadd  12024  climuni  12042  reccn2ap  12062  isumz  12139  geoisum1c  12270  prod1dc  12336  efltim  12448  dvdsval2  12540  dvdscmulr  12570  dvdsmulcr  12571  modmulconst  12573  dvdsadd2b  12590  dvdsexp  12611  mulmoddvds  12613  divalglemeuneg  12673  gcdaddm  12744  dvdsgcdb  12773  mulgcd  12776  gcddiv  12779  uzwodc  12797  lcmdvdsb  12845  mulgcddvds  12855  qredeq  12857  divgcdcoprm0  12862  cncongr1  12864  euclemma  12907  rpexp  12914  rpexp12i  12916  fermltl  12995  prmdiv  12996  odzcllem  13004  odzdvds  13007  odzphi  13008  vfermltl  13013  coprimeprodsq  13019  pythagtriplem6  13032  pythagtriplem7  13033  pythagtriplem12  13037  pythagtriplem13  13038  pceu  13057  pcdvdsb  13082  pcgcd1  13090  dvdsprmpweq  13097  sumhashdc  13109  ctinf  13304  fvsetsid  13369  ressressg  13412  ressabsg  13413  rngplusgg  13474  imasaddvallemg  13619  qusaddvallemg  13637  plusfvalg  13666  mgmb1mgm1  13671  issubmnd  13738  ress0g  13739  imasmnd2  13742  imasmnd  13743  grpasscan2  13852  grpidrcan  13853  grpidlcan  13854  grpinvadd  13866  grpsubeq0  13874  grppncan  13879  dfgrp3mlem  13886  dfgrp3me  13888  grpsubpropd2  13893  imasgrp2  13896  imasgrp  13897  mhmmnd  13902  mulgnn0p1  13919  mulgnnsubcl  13920  mulgnn0subcl  13921  mulgsubcl  13922  mulgneg  13926  mulgaddcom  13932  mulginvcom  13933  submmulg  13952  subgcl  13970  subgsubcl  13971  subgsub  13972  subgmulg  13974  nsgconj  13992  nsgid  14001  quseccl0g  14017  ghmmulg  14042  ghmeqker  14057  f1ghm0to0  14058  kerf1ghm  14060  ablinvadd  14097  ablsub4  14100  ablpncan2  14103  subgabl  14119  gzsumconst  14126  gsumsncmn  14139  gsumconstcmn  14149  pwsinvg  14198  rngcl  14226  imasrng  14238  srgcl  14257  ringcl  14300  crngcom  14301  ringidss  14317  ringcom  14319  imasring  14352  opprringbg  14368  unitmulcl  14403  unitmulclb  14404  dvrcl  14425  unitdvcl  14426  dvrcan1  14430  dvrcan3  14431  rhmmul  14454  subrngrng  14493  subrngmcl  14500  subrgmcl  14524  subrgdv  14529  rrgeq0  14556  domneq0  14564  islmod  14610  scafvalg  14627  lmodcom  14653  rmodislmodlem  14670  rmodislmod  14671  lssclg  14684  lssvnegcl  14696  lssintclm  14704  lspss  14719  lspun  14722  lspsnvsi  14738  rspssp  14814  rnglidlmmgm  14816  rnglidlmsgrp  14817  rnglidlrng  14818  zndvds  14967  aspss  15002  asclmul1  15012  asclmul2  15013  ascldimul  15014  asclinvg  15015  asclmulg  15027  psrbaglecl  15043  psrbagcon  15045  2basgeng  15166  iuncld  15199  ntrss  15203  restco  15258  restabs  15259  cnprcl2k  15290  lmconst  15300  cnrest2  15320  cnmpt2t  15377  psmetsym  15413  psmetge0  15415  xmetge0  15449  xmetsym  15452  blvalps  15472  blval  15473  xblcntrps  15497  xblcntr  15498  xmssym  15553  blsscls2  15577  bdxmet  15585  txmetcnp  15602  dvfvalap  15765  dvid  15779  dvidre  15781  dvcnp2cntop  15783  elplyr  15824  logfac  15978  rpcxpadd  15990  rpcxpsub  15993  rpmulcxp  15994  rpdivcxp  15996  cxpmul  15997  rpcxple2  16003  rpcxplt2  16004  rplogbval  16030  rplogbcl  16031  rplogbreexp  16038  relogbexpap  16043  logbleb  16046  logblt  16047  rplogbcxp  16048  rpcxplogb  16049  relogbcxpbap  16050  sgmppw  16089  lgsneg1  16127  lgsmod  16128  lgsne0  16140  lgssq  16142  lgsdirnn0  16149  lgsdinn0  16150  lgsquad  16182  funvtxvalg  16260  funiedgvalg  16261  lpvtx  16303  ausgrumgrien  16394  ausgrusgrien  16395  uhgrissubgr  16485  egrsubgr  16487  subumgredg2en  16495  subusgr  16499  wlkl1loop  16582  clwwlknonex2  16663  eulerpathprum  16704  eulerpathum  16705  findset  16954  repiecele0  17049  repiecege0  17050