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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 471 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 1076 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simpl3l  1108  simpr3l  1114  simp13l  1168  simp23l  1174  simp33l  1180  tfisi  6924  tfrlem5  7337  omeulem1  7523  omeulem2  7524  uniinqs  7688  elfiun  8193  tcrank  8604  isfin2-2  8998  konigthlem  9243  gruen  9487  addid2  10067  mulcan  10510  mulcan2  10511  divass  10549  divdir  10556  div11  10559  muldivdir  10566  divcan5  10573  ltmul1  10719  ltdiv1  10733  ltmuldiv  10742  lediv2  10759  xaddass2  11906  xlt2add  11916  xmulasslem3  11942  xadddi2  11953  expaddz  12718  expmulz  12720  muldivbinom2  12861  resqrtcl  13785  o1add  14135  o1mul  14136  o1sub  14137  dvdsadd2b  14809  dvdsgcd  15042  rpexp12i  15215  pythagtriplem3  15304  pcpremul  15329  pceu  15332  pcqmul  15339  pcqdiv  15343  f1ocpbllem  15950  funcoppc  16301  funcres  16322  catcisolem  16522  1stfcl  16603  2ndfcl  16604  prfcl  16609  evlfcl  16628  curf1cl  16634  curfcl  16638  hofcl  16665  latjlej12  16833  latmlem12  16849  latj4  16867  latj4rot  16868  symgsssg  17653  symgfisg  17654  psgnunilem4  17683  odcong  17734  cmn4  17978  ablsub4  17984  abladdsub4  17985  lsm4  18029  abvdom  18604  abvres  18605  abvtrivd  18606  lspsolvlem  18906  lbsextlem2  18923  lidlsubcl  18980  frlmbas3  19873  matmulcell  20009  marrepeval  20127  ma1repveval  20135  submaeval  20146  mdetunilem3  20178  mdetuni0  20185  mdetmul  20187  minmar1eval  20213  nllyrest  21038  hausflimlem  21532  tsmsxp  21707  psmetlecl  21869  xmetlecl  21899  prdsxmetlem  21921  bndth  22493  cph2ass  22741  iscau3  22799  dvres2  23396  coemullem  23724  vieta1  23785  aalioulem4  23808  cxpcn3lem  24202  angcan  24246  dchrvmasumlema  24903  logdivsum  24936  abvcxp  25018  padicabv  25033  ax5seglem3  25526  ax5seglem6  25529  axpasch  25536  axeuclid  25558  axcontlem4  25562  axcontlem8  25566  clwwlknimp  26067  adjlnop  28132  xreceu  28764  orngmul  28937  rhmdvd  28955  measvunilem  29405  measvunilem0  29406  measres  29415  bnj1128  30115  subdivcomb1  30667  subdivcomb2  30668  cgrcomim  31069  cgrcoml  31076  cgrcomr  31077  cgrdegen  31084  segconeu  31091  btwnintr  31099  btwnexch3  31100  btwnouttr2  31102  btwnouttr  31104  btwnexch  31105  trisegint  31108  lineext  31156  linecgr  31161  lineid  31163  idinside  31164  btwnconn1lem3  31169  btwnconn1lem4  31170  btwnconn1lem7  31173  btwnconn1lem14  31180  btwnconn2  31182  midofsegid  31184  btwnoutside  31205  outsideoftr  31209  lineunray  31227  lineelsb2  31228  cnres2  32532  heibor  32590  lsmcv2  33134  lcvat  33135  lcvexchlem4  33142  lcvexchlem5  33143  lfladd  33171  lflsub  33172  lflmul  33173  lshpkrlem4  33218  latm4  33338  omlmod1i2N  33365  cvlatexch3  33443  cvlsupr7  33453  hlatj4  33478  hlrelat3  33516  cvrval3  33517  atcvrj1  33535  atlelt  33542  2atlt  33543  2atjm  33549  3noncolr2  33553  athgt  33560  3dimlem2  33563  3dimlem4  33568  3dimlem4OLDN  33569  3dim3  33573  1cvratex  33577  ps-1  33581  ps-2  33582  hlatexch3N  33584  llnle  33622  atcvrlln2  33623  atcvrlln  33624  lplni2  33641  lplnle  33644  lplnnle2at  33645  llncvrlpln2  33661  lplnexllnN  33668  2llnmeqat  33675  lvolnle3at  33686  4atlem0ae  33698  lplncvrlvol2  33719  lnjatN  33884  lncvrat  33886  cdlemblem  33897  elpaddri  33906  paddasslem2  33925  paddasslem16  33939  padd4N  33944  hlmod1i  33960  dalawlem2  33976  pclfinN  34004  pexmidlem4N  34077  pl42lem1N  34083  lhp2lt  34105  lhpexle1  34112  lhpexle2lem  34113  lhpj1  34126  lhpmcvr5N  34131  lhp2at0  34136  lhp2atnle  34137  lhp2at0nle  34139  lhple  34146  lhpat  34147  lhpat4N  34148  4atexlempnq  34159  4atexlem7  34179  4atex  34180  ltrn11  34230  ltrnle  34233  ltrnm  34235  ltrnj  34236  ltrncvr  34237  ltrnel  34243  ltrncnvel  34246  ltrncnv  34250  ltrnmwOLD  34256  trlval2  34268  trlcnv  34270  trljat1  34271  trljat2  34272  trlat  34274  trl0  34275  trlnidat  34278  trlnid  34284  cdlemc1  34296  cdlemc2  34297  cdlemc5  34300  cdlemd2  34304  cdlemd7  34309  cdlemd8  34310  cdlemd9  34311  cdleme0e  34322  cdleme3g  34339  cdleme3h  34340  cdleme3  34342  cdleme5  34345  cdleme10  34359  cdleme11a  34365  cdleme11c  34366  cdleme11h  34371  cdleme11j  34372  cdleme0nex  34395  cdleme18a  34396  cdleme18b  34397  cdleme22gb  34399  cdleme20zN  34406  cdleme20yOLD  34408  cdleme20c  34417  cdleme20k  34425  cdleme21a  34431  cdleme21b  34432  cdleme21c  34433  cdleme21h  34440  cdleme22b  34447  cdleme22d  34449  cdleme22f  34452  cdleme25a  34459  cdleme25c  34461  cdleme25dN  34462  cdleme26ee  34466  cdleme30a  34484  cdlemefr29bpre0N  34512  cdlemefr29clN  34513  cdlemefr32fvaN  34515  cdlemefr32fva1  34516  cdlemefs29bpre0N  34522  cdlemefs29bpre1N  34523  cdlemefs29cpre1N  34524  cdlemefs29clN  34525  cdleme43fsv1snlem  34526  cdlemefs32fvaN  34528  cdlemefs32fva1  34529  cdlemefs31fv1  34530  cdleme36a  34566  cdleme39a  34571  cdleme42a  34577  cdleme42c  34578  cdleme17d3  34602  cdleme48fv  34605  cdleme48bw  34608  cdleme48b  34609  cdlemeg46rgv  34634  cdlemeg46req  34635  cdlemeg46gfv  34636  cdleme48d  34641  cdleme50trn2a  34656  cdleme50trn2  34657  cdleme50ltrn  34663  cdlemf1  34667  cdlemf  34669  trlord  34675  cdlemg2dN  34696  cdlemg2fvlem  34700  cdlemg2l  34709  cdlemg7fvbwN  34713  cdlemg7aN  34731  cdlemg10bALTN  34742  cdlemg10c  34745  cdlemg17a  34767  cdlemg17dALTN  34770  cdlemg31b0a  34801  cdlemg31a  34803  cdlemg31b  34804  cdlemg34  34818  cdlemg36  34820  ltrnco  34825  trlcoabs2N  34828  trlcolem  34832  cdlemg48  34843  tgrpov  34854  tendoco2  34874  tendoplco2  34885  cdlemh1  34921  cdlemi1  34924  cdlemi2  34925  cdlemj3  34929  tendoid0  34931  cdlemk1  34937  cdlemk2  34938  cdlemk4  34940  cdlemk8  34944  cdlemk9  34945  cdlemk9bN  34946  cdlemk10  34949  cdlemk26b-3  35011  cdlemk26-3  35012  cdlemk28-3  35014  cdlemk37  35020  cdlemk39  35022  cdlemkfid1N  35027  cdlemkid1  35028  cdlemky  35032  cdlemkyu  35033  cdlemk19ylem  35036  cdlemk19xlem  35048  cdlemk11t  35052  cdlemk51  35059  cdlemkyyN  35068  cdleml6  35087  cdleml7  35088  cdleml8  35089  cdleml9  35090  erngdvlem4  35097  erngdvlem4-rN  35105  tendospcanN  35130  dia11N  35155  cdlemm10N  35225  dib11N  35267  dicvaddcl  35297  dicvscacl  35298  cdlemn6  35309  dihvalcq2  35354  dihopelvalcpre  35355  dihord6b  35367  dihord5apre  35369  dihmeetlem1N  35397  dihmeetlem2N  35406  dihglbcpreN  35407  dihjatc1  35418  dihmeetlem20N  35433  dih1dimatlem0  35435  dihatlat  35441  dihglblem6  35447  dochexmidlem4  35570  mapdpglem32  35812  mapdh8ad  35886  mapdh9aOLDN  35898  hdmap11lem2  35952  hdmap14lem6  35983  mzpsubst  36129  pellex  36217  pellfundex  36268  pellfund14gap  36269  qirropth  36291  rmxypos  36332  congmul  36352  congsub  36355  mzpcong  36357  coprmdvdsb  36370  jm2.15nn0  36388  jm2.16nn0  36389  rpnnen3lem  36416  idomsubgmo  36595  relexp01min  36824  mullimc  38484  islptre  38487  limccog  38488  mullimcf  38491  addlimc  38516  0ellimcdiv  38517  stoweidlem57  38751  fourierdlem48  38848  fourierdlem80  38880  fourierdlem113  38913  ovncvrrp  39255  opnvonmbllem2  39324  ovolval5lem3  39345  ovnovollem3  39349  1wlkl1loop  40841  trlsonwlkon  40916  pthontrlon  40952  wspthsswwlknon  41127
  Copyright terms: Public domain W3C validator