MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3l Structured version   Visualization version   GIF version

Theorem simp3l 1193
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 483 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 1127 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simp13l  1280  simp23l  1286  simp33l  1292  tfisi  7561  tfrlem5  8007  omeulem1  8198  omeulem2  8199  uniinqs  8367  elfiun  8883  tcrank  9302  isfin2-2  9730  konigthlem  9979  gruen  10223  addid2  10812  mulcan  11266  mulcan2  11267  divass  11305  divdir  11312  div11  11315  muldivdir  11322  subdivcomb1  11324  subdivcomb2  11325  divcan5  11331  ltmul1  11479  ltdiv1  11493  ltmuldiv  11502  lediv2  11519  xaddass2  12633  xlt2add  12643  xmulasslem3  12669  xadddi2  12680  expaddz  13463  expmulz  13465  muldivbinom2  13613  resqrtcl  14603  o1add  14960  o1mul  14961  o1sub  14962  dvdsadd2b  15646  dvdsgcd  15882  rpexp12i  16056  pythagtriplem3  16145  pcpremul  16170  pceu  16173  pcqmul  16180  pcqdiv  16184  setsstruct  16513  f1ocpbllem  16787  funcoppc  17135  funcres  17156  catcisolem  17356  1stfcl  17437  2ndfcl  17438  prfcl  17443  evlfcl  17462  curf1cl  17468  curfcl  17472  hofcl  17499  latjlej12  17667  latmlem12  17683  latj4  17701  latj4rot  17702  symgsssg  18526  symgfisg  18527  psgnunilem4  18556  odcong  18608  cmn4  18857  ablsub4  18864  abladdsub4  18865  lsm4  18911  abvdom  19540  abvres  19541  abvtrivd  19542  lspsolvlem  19845  lbsextlem2  19862  lidlsubcl  19919  frlmbas3  20850  matmulcell  20984  marrepeval  21102  ma1repveval  21110  submaeval  21121  mdetunilem3  21153  mdetuni0  21160  mdetmul  21162  minmar1eval  21188  nllyrest  22024  hausflimlem  22517  tsmsxp  22692  psmetlecl  22854  xmetlecl  22885  prdsxmetlem  22907  ngpocelbl  23242  bndth  23491  cph2ass  23746  iscau3  23810  dvres2  24439  coemullem  24769  vieta1  24830  aalioulem4  24853  cxpcn3lem  25255  angcan  25307  dchrvmasumlema  26004  logdivsum  26037  abvcxp  26119  padicabv  26134  ax5seglem3  26645  ax5seglem6  26648  axpasch  26655  axeuclid  26677  axcontlem4  26681  axcontlem8  26685  wlkl1loop  27347  trlsonwlkon  27419  pthontrlon  27456  wspthsswwlknon  27628  frgr2wwlkeqm  28038  adjlnop  29791  xreceu  30526  orngmul  30804  rhmdvd  30822  measvunilem  31371  measvunilem0  31372  measres  31381  bnj1128  32160  umgr2cycllem  32285  umgr2cycl  32286  satfv1fvfmla1  32568  fpr3g  33020  nosupbnd1lem4  33109  nosupbnd1lem5  33110  cgrcomim  33348  cgrcoml  33355  cgrcomr  33356  cgrdegen  33363  segconeu  33370  btwnintr  33378  btwnexch3  33379  btwnouttr2  33381  btwnouttr  33383  btwnexch  33384  trisegint  33387  lineext  33435  linecgr  33440  lineid  33442  idinside  33443  btwnconn1lem3  33448  btwnconn1lem4  33449  btwnconn1lem7  33452  btwnconn1lem14  33459  btwnconn2  33461  midofsegid  33463  btwnoutside  33484  outsideoftr  33488  lineunray  33506  lineelsb2  33507  cnres2  34924  heibor  34982  lsmcv2  36047  lcvat  36048  lcvexchlem4  36055  lcvexchlem5  36056  lfladd  36084  lflsub  36085  lflmul  36086  lshpkrlem4  36131  latm4  36251  omlmod1i2N  36278  cvlatexch3  36356  cvlsupr7  36366  hlatj4  36392  hlrelat3  36430  cvrval3  36431  atcvrj1  36449  atlelt  36456  2atlt  36457  2atjm  36463  3noncolr2  36467  athgt  36474  3dimlem2  36477  3dimlem4  36482  3dimlem4OLDN  36483  3dim3  36487  1cvratex  36491  ps-1  36495  ps-2  36496  hlatexch3N  36498  llnle  36536  atcvrlln2  36537  atcvrlln  36538  lplni2  36555  lplnle  36558  lplnnle2at  36559  llncvrlpln2  36575  lplnexllnN  36582  2llnmeqat  36589  lvolnle3at  36600  4atlem0ae  36612  lplncvrlvol2  36633  lnjatN  36798  lncvrat  36800  cdlemblem  36811  elpaddri  36820  paddasslem2  36839  paddasslem16  36853  padd4N  36858  hlmod1i  36874  dalawlem2  36890  pclfinN  36918  pexmidlem4N  36991  pl42lem1N  36997  lhp2lt  37019  lhpexle1  37026  lhpexle2lem  37027  lhpj1  37040  lhpmcvr5N  37045  lhp2at0  37050  lhp2atnle  37051  lhp2at0nle  37053  lhple  37060  lhpat  37061  lhpat4N  37062  4atexlempnq  37073  4atexlem7  37093  4atex  37094  ltrn11  37144  ltrnle  37147  ltrnm  37149  ltrnj  37150  ltrncvr  37151  ltrnel  37157  ltrncnvel  37160  ltrncnv  37164  trlval2  37181  trlcnv  37183  trljat1  37184  trljat2  37185  trlat  37187  trl0  37188  trlnidat  37191  trlnid  37197  cdlemc1  37209  cdlemc2  37210  cdlemc5  37213  cdlemd2  37217  cdlemd7  37222  cdlemd8  37223  cdlemd9  37224  cdleme0e  37235  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme5  37258  cdleme10  37272  cdleme11a  37278  cdleme11c  37279  cdleme11h  37284  cdleme11j  37285  cdleme0nex  37308  cdleme18a  37309  cdleme18b  37310  cdleme22gb  37312  cdleme20zN  37319  cdleme20c  37329  cdleme20k  37337  cdleme21a  37343  cdleme21b  37344  cdleme21c  37345  cdleme21h  37352  cdleme22b  37359  cdleme22d  37361  cdleme22f  37364  cdleme25a  37371  cdleme25c  37373  cdleme25dN  37374  cdleme26ee  37378  cdleme30a  37396  cdlemefr29bpre0N  37424  cdlemefr29clN  37425  cdlemefr32fvaN  37427  cdlemefr32fva1  37428  cdlemefs29bpre0N  37434  cdlemefs29bpre1N  37435  cdlemefs29cpre1N  37436  cdlemefs29clN  37437  cdleme43fsv1snlem  37438  cdlemefs32fvaN  37440  cdlemefs32fva1  37441  cdlemefs31fv1  37442  cdleme36a  37478  cdleme39a  37483  cdleme42a  37489  cdleme42c  37490  cdleme17d3  37514  cdleme48fv  37517  cdleme48bw  37520  cdleme48b  37521  cdlemeg46rgv  37546  cdlemeg46req  37547  cdlemeg46gfv  37548  cdleme48d  37553  cdleme50trn2a  37568  cdleme50trn2  37569  cdleme50ltrn  37575  cdlemf1  37579  cdlemf  37581  trlord  37587  cdlemg2dN  37608  cdlemg2fvlem  37612  cdlemg2l  37621  cdlemg7fvbwN  37625  cdlemg7aN  37643  cdlemg10bALTN  37654  cdlemg10c  37657  cdlemg17a  37679  cdlemg17dALTN  37682  cdlemg31b0a  37713  cdlemg31a  37715  cdlemg31b  37716  cdlemg34  37730  cdlemg36  37732  ltrnco  37737  trlcoabs2N  37740  trlcolem  37744  cdlemg48  37755  tgrpov  37766  tendoco2  37786  tendoplco2  37797  cdlemh1  37833  cdlemi1  37836  cdlemi2  37837  cdlemj3  37841  tendoid0  37843  cdlemk1  37849  cdlemk2  37850  cdlemk4  37852  cdlemk8  37856  cdlemk9  37857  cdlemk9bN  37858  cdlemk10  37861  cdlemk26b-3  37923  cdlemk26-3  37924  cdlemk28-3  37926  cdlemk37  37932  cdlemk39  37934  cdlemkfid1N  37939  cdlemkid1  37940  cdlemky  37944  cdlemkyu  37945  cdlemk19ylem  37948  cdlemk19xlem  37960  cdlemk11t  37964  cdlemk51  37971  cdlemkyyN  37980  cdleml6  37999  cdleml7  38000  cdleml8  38001  cdleml9  38002  erngdvlem4  38009  erngdvlem4-rN  38017  tendospcanN  38041  dia11N  38066  cdlemm10N  38136  dib11N  38178  dicvaddcl  38208  dicvscacl  38209  cdlemn6  38220  dihvalcq2  38265  dihopelvalcpre  38266  dihord6b  38278  dihord5apre  38280  dihmeetlem1N  38308  dihmeetlem2N  38317  dihglbcpreN  38318  dihjatc1  38329  dihmeetlem20N  38344  dih1dimatlem0  38346  dihatlat  38352  dihglblem6  38358  dochexmidlem4  38481  mapdpglem32  38723  mapdh8ad  38797  mapdh9aOLDN  38808  hdmap11lem2  38860  hdmap14lem6  38891  frlmfzowrdb  39023  mzpsubst  39225  pellex  39312  pellfundex  39363  pellfund14gap  39364  qirropth  39385  rmxypos  39424  congmul  39444  congsub  39447  mzpcong  39449  coprmdvdsb  39462  jm2.15nn0  39480  jm2.16nn0  39481  rpnnen3lem  39508  idomsubgmo  39678  relexp01min  39938  mullimc  41777  islptre  41780  limccog  41781  mullimcf  41784  addlimc  41809  0ellimcdiv  41810  limsupre3lem  41893  stoweidlem57  42223  fourierdlem48  42320  fourierdlem80  42352  fourierdlem113  42385  ovncvrrp  42727  opnvonmbllem2  42796  ovolval5lem3  42817  ovnovollem3  42821  itsclc0lem1  44641  itsclc0lem2  44642  itschlc0yqe  44645  itscnhlc0xyqsol  44650  itschlc0xyqsol1  44651
  Copyright terms: Public domain W3C validator