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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 486 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 1132 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simp13l  1285  simp23l  1291  simp33l  1297  tfisi  7567  tfrlem5  8012  omeulem1  8204  omeulem2  8205  uniinqs  8373  elfiun  8891  tcrank  9310  isfin2-2  9739  konigthlem  9988  gruen  10232  addid2  10821  mulcan  11275  mulcan2  11276  divass  11314  divdir  11321  div11  11324  muldivdir  11331  subdivcomb1  11333  subdivcomb2  11334  divcan5  11340  ltmul1  11488  ltdiv1  11502  ltmuldiv  11511  lediv2  11528  xaddass2  12640  xlt2add  12650  xmulasslem3  12676  xadddi2  12687  expaddz  13478  expmulz  13480  muldivbinom2  13628  resqrtcl  14613  o1add  14970  o1mul  14971  o1sub  14972  dvdsadd2b  15656  dvdsgcd  15890  rpexp12i  16064  pythagtriplem3  16153  pcpremul  16178  pceu  16181  pcqmul  16188  pcqdiv  16192  setsstruct  16523  f1ocpbllem  16797  funcoppc  17145  funcres  17166  catcisolem  17366  1stfcl  17447  2ndfcl  17448  prfcl  17453  evlfcl  17472  curf1cl  17478  curfcl  17482  hofcl  17509  latjlej12  17677  latmlem12  17693  latj4  17711  latj4rot  17712  symgsssg  18595  symgfisg  18596  psgnunilem4  18625  odcong  18677  cmn4  18926  ablsub4  18933  abladdsub4  18934  lsm4  18980  abvdom  19609  abvres  19610  abvtrivd  19611  lspsolvlem  19914  lbsextlem2  19931  lidlsubcl  19989  frlmbas3  20920  matmulcell  21054  marrepeval  21172  ma1repveval  21180  submaeval  21191  mdetunilem3  21223  mdetuni0  21230  mdetmul  21232  minmar1eval  21258  nllyrest  22094  hausflimlem  22587  tsmsxp  22763  psmetlecl  22925  xmetlecl  22956  prdsxmetlem  22978  ngpocelbl  23313  bndth  23566  cph2ass  23821  iscau3  23885  dvres2  24518  coemullem  24850  vieta1  24911  aalioulem4  24934  cxpcn3lem  25339  angcan  25391  dchrvmasumlema  26087  logdivsum  26120  abvcxp  26202  padicabv  26217  ax5seglem3  26728  ax5seglem6  26731  axpasch  26738  axeuclid  26760  axcontlem4  26764  axcontlem8  26768  wlkl1loop  27430  trlsonwlkon  27502  pthontrlon  27539  wspthsswwlknon  27710  frgr2wwlkeqm  28119  adjlnop  29872  xreceu  30609  orngmul  30909  rhmdvd  30927  measvunilem  31528  measvunilem0  31529  measres  31538  bnj1128  32319  umgr2cycllem  32444  umgr2cycl  32445  satfv1fvfmla1  32727  fpr3g  33179  nosupbnd1lem4  33268  nosupbnd1lem5  33269  cgrcomim  33507  cgrcoml  33514  cgrcomr  33515  cgrdegen  33522  segconeu  33529  btwnintr  33537  btwnexch3  33538  btwnouttr2  33540  btwnouttr  33542  btwnexch  33543  trisegint  33546  lineext  33594  linecgr  33599  lineid  33601  idinside  33602  btwnconn1lem3  33607  btwnconn1lem4  33608  btwnconn1lem7  33611  btwnconn1lem14  33618  btwnconn2  33620  midofsegid  33622  btwnoutside  33643  outsideoftr  33647  lineunray  33665  lineelsb2  33666  cnres2  35146  heibor  35204  lsmcv2  36270  lcvat  36271  lcvexchlem4  36278  lcvexchlem5  36279  lfladd  36307  lflsub  36308  lflmul  36309  lshpkrlem4  36354  latm4  36474  omlmod1i2N  36501  cvlatexch3  36579  cvlsupr7  36589  hlatj4  36615  hlrelat3  36653  cvrval3  36654  atcvrj1  36672  atlelt  36679  2atlt  36680  2atjm  36686  3noncolr2  36690  athgt  36697  3dimlem2  36700  3dimlem4  36705  3dimlem4OLDN  36706  3dim3  36710  1cvratex  36714  ps-1  36718  ps-2  36719  hlatexch3N  36721  llnle  36759  atcvrlln2  36760  atcvrlln  36761  lplni2  36778  lplnle  36781  lplnnle2at  36782  llncvrlpln2  36798  lplnexllnN  36805  2llnmeqat  36812  lvolnle3at  36823  4atlem0ae  36835  lplncvrlvol2  36856  lnjatN  37021  lncvrat  37023  cdlemblem  37034  elpaddri  37043  paddasslem2  37062  paddasslem16  37076  padd4N  37081  hlmod1i  37097  dalawlem2  37113  pclfinN  37141  pexmidlem4N  37214  pl42lem1N  37220  lhp2lt  37242  lhpexle1  37249  lhpexle2lem  37250  lhpj1  37263  lhpmcvr5N  37268  lhp2at0  37273  lhp2atnle  37274  lhp2at0nle  37276  lhple  37283  lhpat  37284  lhpat4N  37285  4atexlempnq  37296  4atexlem7  37316  4atex  37317  ltrn11  37367  ltrnle  37370  ltrnm  37372  ltrnj  37373  ltrncvr  37374  ltrnel  37380  ltrncnvel  37383  ltrncnv  37387  trlval2  37404  trlcnv  37406  trljat1  37407  trljat2  37408  trlat  37410  trl0  37411  trlnidat  37414  trlnid  37420  cdlemc1  37432  cdlemc2  37433  cdlemc5  37436  cdlemd2  37440  cdlemd7  37445  cdlemd8  37446  cdlemd9  37447  cdleme0e  37458  cdleme3g  37475  cdleme3h  37476  cdleme3  37478  cdleme5  37481  cdleme10  37495  cdleme11a  37501  cdleme11c  37502  cdleme11h  37507  cdleme11j  37508  cdleme0nex  37531  cdleme18a  37532  cdleme18b  37533  cdleme22gb  37535  cdleme20zN  37542  cdleme20c  37552  cdleme20k  37560  cdleme21a  37566  cdleme21b  37567  cdleme21c  37568  cdleme21h  37575  cdleme22b  37582  cdleme22d  37584  cdleme22f  37587  cdleme25a  37594  cdleme25c  37596  cdleme25dN  37597  cdleme26ee  37601  cdleme30a  37619  cdlemefr29bpre0N  37647  cdlemefr29clN  37648  cdlemefr32fvaN  37650  cdlemefr32fva1  37651  cdlemefs29bpre0N  37657  cdlemefs29bpre1N  37658  cdlemefs29cpre1N  37659  cdlemefs29clN  37660  cdleme43fsv1snlem  37661  cdlemefs32fvaN  37663  cdlemefs32fva1  37664  cdlemefs31fv1  37665  cdleme36a  37701  cdleme39a  37706  cdleme42a  37712  cdleme42c  37713  cdleme17d3  37737  cdleme48fv  37740  cdleme48bw  37743  cdleme48b  37744  cdlemeg46rgv  37769  cdlemeg46req  37770  cdlemeg46gfv  37771  cdleme48d  37776  cdleme50trn2a  37791  cdleme50trn2  37792  cdleme50ltrn  37798  cdlemf1  37802  cdlemf  37804  trlord  37810  cdlemg2dN  37831  cdlemg2fvlem  37835  cdlemg2l  37844  cdlemg7fvbwN  37848  cdlemg7aN  37866  cdlemg10bALTN  37877  cdlemg10c  37880  cdlemg17a  37902  cdlemg17dALTN  37905  cdlemg31b0a  37936  cdlemg31a  37938  cdlemg31b  37939  cdlemg34  37953  cdlemg36  37955  ltrnco  37960  trlcoabs2N  37963  trlcolem  37967  cdlemg48  37978  tgrpov  37989  tendoco2  38009  tendoplco2  38020  cdlemh1  38056  cdlemi1  38059  cdlemi2  38060  cdlemj3  38064  tendoid0  38066  cdlemk1  38072  cdlemk2  38073  cdlemk4  38075  cdlemk8  38079  cdlemk9  38080  cdlemk9bN  38081  cdlemk10  38084  cdlemk26b-3  38146  cdlemk26-3  38147  cdlemk28-3  38149  cdlemk37  38155  cdlemk39  38157  cdlemkfid1N  38162  cdlemkid1  38163  cdlemky  38167  cdlemkyu  38168  cdlemk19ylem  38171  cdlemk19xlem  38183  cdlemk11t  38187  cdlemk51  38194  cdlemkyyN  38203  cdleml6  38222  cdleml7  38223  cdleml8  38224  cdleml9  38225  erngdvlem4  38232  erngdvlem4-rN  38240  tendospcanN  38264  dia11N  38289  cdlemm10N  38359  dib11N  38401  dicvaddcl  38431  dicvscacl  38432  cdlemn6  38443  dihvalcq2  38488  dihopelvalcpre  38489  dihord6b  38501  dihord5apre  38503  dihmeetlem1N  38531  dihmeetlem2N  38540  dihglbcpreN  38541  dihjatc1  38552  dihmeetlem20N  38567  dih1dimatlem0  38569  dihatlat  38575  dihglblem6  38581  dochexmidlem4  38704  mapdpglem32  38946  mapdh8ad  39020  mapdh9aOLDN  39031  hdmap11lem2  39083  hdmap14lem6  39114  frlmfzowrdb  39371  mzpsubst  39605  pellex  39692  pellfundex  39743  pellfund14gap  39744  qirropth  39765  rmxypos  39804  congmul  39824  congsub  39827  mzpcong  39829  coprmdvdsb  39842  jm2.15nn0  39860  jm2.16nn0  39861  rpnnen3lem  39888  idomsubgmo  40058  relexp01min  40330  mullimc  42184  islptre  42187  limccog  42188  mullimcf  42191  addlimc  42216  0ellimcdiv  42217  limsupre3lem  42300  stoweidlem57  42625  fourierdlem48  42722  fourierdlem80  42754  fourierdlem113  42787  ovncvrrp  43129  opnvonmbllem2  43198  ovolval5lem3  43219  ovnovollem3  43223  itsclc0lem1  45096  itsclc0lem2  45097  itschlc0yqe  45100  itscnhlc0xyqsol  45105  itschlc0xyqsol1  45106
  Copyright terms: Public domain W3C validator