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

Theorem simpl3 1190
Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpl3 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3
StepHypRef Expression
1 simpl 486 . 2 ((𝜒𝜃) → 𝜒)
213ad2antl3 1184 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:  simpl13  1247  simpl23  1250  simpl33  1253  simp1l3  1265  simp2l3  1271  simp3l3  1277  3anandirs  1469  2nreu  4374  f1prex  7022  fcofo  7026  soisores  7062  weniso  7089  knatar  7092  ofmpteq  7411  funelss  7729  smorndom  7988  nnmord  8241  nnmword  8242  difsnen  8582  mapunen  8670  ac6sfi  8746  fipreima  8814  wemaplem2  8995  wemapso2lem  9000  en2eqpr  9418  indcardi  9452  acndom  9462  fodomfi2  9471  infmap2  9625  cflim2  9670  coftr  9680  infpssrlem4  9713  fin23lem11  9724  fincssdom  9730  isf32lem9  9768  fin1a2lem9  9815  gchpwdom  10077  gruima  10209  prpssnq  10397  distrlem4pr  10433  dedekind  10788  addcan  10809  addcan2  10810  divmulass  11306  supmul1  11595  uzsupss  12326  xaddass  12628  xleadd1a  12632  xlesubadd  12642  xmulasslem3  12665  xmulass  12666  xadddilem  12673  xadddi  12674  ixxun  12740  icoshftf1o  12850  snunioc  12856  difelfzle  13013  fzo1fzo0n0  13081  ssfzoulel  13124  modmuladd  13274  modifeq2int  13294  modaddmulmod  13299  modsubdir  13301  ltexp2a  13524  leexp2  13529  ltexp2r  13531  exple1  13534  expnlbnd2  13589  mulsubdivbinom2  13616  hashtpg  13837  ccatass  13931  ccatopth  14067  pfxccatin12lem2a  14078  pfxccat3  14085  cshinj  14162  2cshw  14164  s2f1o  14267  limsupgre  14827  addcn2  14939  mulcn2  14941  binomrisefac  15385  bpolydif  15398  dvdsmodexp  15604  modmulconst  15630  dvdsmod  15667  sadass  15807  gcdass  15882  rplpwr  15894  rppwr  15895  rpmulgcd2  15987  rpdvds  15991  rpexp  16051  prmdiveq  16110  hashgcdlem  16112  coprimeprodsq  16132  coprimeprodsq2  16133  pythagtriplem3  16142  pcdvdsb  16192  pcgcd1  16200  dvdsprmpweq  16207  pcbc  16223  0ram  16343  ramz2  16347  ramub1lem1  16349  mremre  16864  mrieqv2d  16899  lubun  17722  isnsgrp  17894  issubmnd  17927  gsumccatOLD  17994  frmdss2  18017  submefmnd  18049  sgrp2rid2ex  18081  mulgnn0p1  18228  mulgnnsubcl  18229  mulgneg  18235  mulgdirlem  18247  nmzsubg  18306  ghmmulg  18359  pmtrfv  18569  pmtrmvd  18573  pmtrfb  18582  odmodnn0  18657  oddvdsnn0  18661  odnncl  18662  odmod  18663  oddvds  18664  odeq  18667  odmulgid  18670  odmulg  18672  odmulgeq  18673  odbezout  18674  odf1o1  18686  odf1o2  18687  odngen  18691  odcau  18718  pgpssslw  18728  fislw  18739  lsmless1x  18758  lsmless2x  18759  lsmsubm  18767  lsmmod  18790  lsmmod2  18791  efgsfo  18854  cntzcmn  18949  odadd1  18957  odadd2  18958  odadd  18959  lsmcomx  18965  prdscmnd  18970  gsumconst  19043  ring1eq0  19329  cntzsubr  19554  isabvd  19577  rmodislmod  19688  lspss  19742  0lmhm  19798  reslmhm2  19811  pwssplit0  19816  pwssplit1  19817  lbspss  19840  lspfixed  19886  lsmcv  19899  lspsnat  19903  issubassa  20084  aspss  20092  coe1subfv  20420  coe1tm  20427  xrsdsreclblem  20577  obselocv  20858  frlmsplit2  20903  frlmsslss2  20905  frlmup4  20931  lindff1  20950  lsslindf  20960  lsslinds  20961  islindf4  20968  mpomatmul  21041  mamutpos  21053  submaval  21176  mdetdiag  21194  mdetunilem1  21207  mdetunilem3  21209  mdetunilem9  21215  mdetmul  21218  maducoeval2  21235  madurid  21239  minmar1val  21243  cramer  21286  cpmatel2  21307  m2cpm  21335  decpmatmul  21366  pmatcollpw1lem2  21369  pmatcollpw1  21370  pmatcollpw2lem  21371  pm2mpcl  21391  mply1topmatcl  21399  mp2pm2mplem2  21401  mp2pm2mplem4  21403  pm2mpghmlem2  21406  pm2mpghmlem1  21407  cayhamlem2  21478  neiint  21698  topssnei  21718  cnrest2  21880  cnprest2  21884  cnt0  21940  cnt1  21944  cnhaus  21948  cncmp  21986  fiuncmp  21998  sscmp  21999  hauscmp  22001  cnconn  22016  unconn  22023  comppfsc  22126  kgen2ss  22149  ptpjopn  22206  ptrescn  22233  qtopss  22309  kqfvima  22324  r0cld  22332  cmphaushmeo  22394  fbssint  22432  fbasrn  22478  filuni  22479  ufilmax  22501  fin1aufil  22526  fmf  22539  fmss  22540  rnelfmlem  22546  rnelfm  22547  fmufil  22553  fmco  22555  flimss2  22566  flimss1  22567  flimrest  22577  cnpflf2  22594  cnpflf  22595  flfcnp  22598  lmflf  22599  supnfcls  22614  fclsss1  22616  fclsss2  22617  cnpfcfi  22634  subgntr  22701  opnsubg  22702  cldsubg  22705  ustuqtop1  22836  ucncn  22880  bldisj  22994  blgt0  22995  bl2in  22996  blss2ps  22999  blss2  23000  xbln0  23010  blssps  23020  blss  23021  lpbl  23099  blcld  23101  blcls  23102  stdbdmopn  23114  metcnp2  23138  txmetcnp  23143  blval2  23158  restmetu  23166  nmoix  23324  nmoi2  23325  nmoeq0  23331  nmotri  23334  metdsge  23443  metds0  23444  metdseq0  23448  icoopnst  23533  iccpnfhmeo  23539  xrhmeo  23540  nmhmcn  23714  cphsqrtcl2  23780  cphsqrtcl3  23781  fmcfil  23865  bcthlem5  23921  cmetcusp1  23946  cssbn  23968  pjth  24032  ovolunnul  24093  volun  24138  voliunlem2  24144  itg2const  24333  iblconst  24410  itgconst  24411  limcvallem  24463  dvcnp2  24512  dvcn  24513  deg1mul3le  24706  deg1tmle  24707  ig1pdvds  24766  coe11  24839  dgrmulc  24857  dvply1  24869  aaliou2  24925  efcvx  25033  tanord  25119  logdivlti  25200  logccv  25243  recxpcl  25255  cxplea  25276  cxple2a  25279  ang180  25389  isosctrlem2  25394  cxp2lim  25551  amgm  25565  muval1  25707  dvdssqf  25712  mumullem2  25754  bcmono  25850  lgsneg  25894  lgsmod  25896  lgsdirprm  25904  lgsdir  25905  lgsdi  25907  brbtwn2  26688  colinearalglem1  26689  colinearalg  26693  axcgrtr  26698  axcontlem2  26748  upgrewlkle2  27385  wlksoneq1eq2  27443  crctcshwlkn0lem5  27589  wspthsnwspthsnon  27691  lppthon  27925  upgriseupth  27981  4cyclusnfrgr  28066  numclwwlk1lem2foa  28128  numclwwlk5  28162  nvmul0or  28422  shless  29131  shlej1  29132  pjspansn  29349  kbmul  29727  homco2  29749  kbass2  29889  fnpreimac  30413  padct  30452  eliccelico  30497  elicoelioo  30498  iocinioc2  30499  difioo  30502  swrdrn2  30625  swrdrn3  30626  xrge0npcan  30699  isarchi2  30832  archiabl  30845  pidlnz  30956  lindssn  30958  ssmxidl  31000  mdetlap1  31112  pstmfval  31157  fmcncfil  31192  zrhnm  31228  qqhnm  31249  nexple  31286  volfiniune  31507  omsmeas  31599  eulerpartlemb  31644  probinc  31697  cndprob01  31711  signswmnd  31845  cvmsss2  32539  dvdspw  33000  funsseq  33029  frpomin  33096  frrlem10  33150  fprlem1  33155  sltres  33187  nolt02olem  33216  nolt02o  33217  nosupbnd1lem1  33226  nosupbnd1lem4  33229  nosupbnd1lem5  33230  nosupbnd1lem6  33231  cgrtriv  33481  5segofs  33485  btwntriv2  33491  btwnxfr  33535  segcon2  33584  brsegle2  33588  seglelin  33595  outsideofeu  33610  lindsenlbs  34952  mblfinlem2  34995  blbnd  35125  rrndstprj2  35169  zerdivemp1x  35285  lsmsat  36204  lsatfixedN  36205  lssat  36212  lkrlsp  36298  lshpkrlem4  36309  cvrcon3b  36473  leat3  36491  atlen0  36506  atnle  36513  atlatmstc  36515  atlatle  36516  cvlcvr1  36535  cvlsupr2  36539  hlsupr2  36583  hlrelat2  36599  cvrexchlem  36615  cvratlem  36617  lnnat  36623  atexchcvrN  36636  1cvratlt  36670  1cvrjat  36671  3atlem3  36681  3atlem7  36685  llni2  36708  atcvrlln2  36715  llnexatN  36717  llncmp  36718  2llnmat  36720  2at0mat0  36721  2atnelpln  36740  llncvrlpln2  36753  2lplnmN  36755  2llnmj  36756  lplncmp  36758  lplnexatN  36759  2llnjaN  36762  lvoli3  36773  islvol2aN  36788  4atlem3a  36793  4atlem4a  36795  4atlem4b  36796  4atlem11  36805  4atlem12  36808  lplncvrlvol2  36811  lvolcmp  36813  2lplnmj  36818  islinei  36936  linepmap  36971  lneq2at  36974  2llnma3r  36984  elpaddn0  36996  elpaddatriN  36999  elpaddat  37000  paddcom  37009  paddss1  37013  paddss2  37014  paddasslem6  37021  paddasslem7  37022  paddasslem10  37025  paddasslem15  37030  pmodlem2  37043  pmodl42N  37047  pmapjoin  37048  atmod1i1m  37054  llnmod1i2  37056  llnexchb2lem  37064  polcon2bN  37116  pclfinclN  37146  poml4N  37149  poml6N  37151  osumcllem11N  37162  osumclN  37163  pmapojoinN  37164  pexmidlem2N  37167  pexmidlem3N  37168  pexmidlem4N  37169  pexmidlem6N  37171  pexmidlem7N  37172  pl42lem2N  37176  pl42lem3N  37177  pl42lem4N  37178  pl42N  37179  lhpexle3lem  37207  lhpmcvr3  37221  lhp2at0nle  37231  lhprelat3N  37236  lauteq  37291  lautco  37293  ltrncoidN  37324  ltrneq2  37344  ltrnnidn  37370  ltrnideq  37371  trlnle  37382  cdlemc  37393  cdlemd4  37397  cdlemd5  37398  cdlemd9  37402  cdlemd  37403  ltrneq3  37404  cdlemefrs29pre00  37591  cdlemefrs29cpre1  37594  cdlemefrs29clN  37595  cdlemefrs32fva  37596  cdlemefr29exN  37598  cdlemefr27cl  37599  cdlemefs27cl  37609  cdlemefs32sn1aw  37610  cdleme32fva  37633  cdleme32d  37640  cdleme32f  37642  cdleme32le  37643  cdleme40n  37664  cdleme41snaw  37672  cdleme17d3  37692  cdleme48fvg  37696  cdlemeg46fvcl  37702  cdlemeg46fgN  37730  cdleme48fgv  37734  ltrniotavalbN  37780  cdlemb3  37802  cdlemg15  37852  cdlemg17dN  37859  trlco  37923  cdlemg44b  37928  ltrncom  37934  trljco  37936  tendococl  37968  tendoplcl  37977  tendoplcom  37978  tendotr  38026  cdlemk36  38109  cdlemk35s-id  38134  cdlemk39s-id  38136  cdlemk19x  38139  cdlemk53b  38152  cdlemk55  38157  cdlemk35u  38160  cdlemk55u  38162  cdlemk39u  38164  cdlemk19u  38166  cdlemk56  38167  tendoex  38171  cdleml5N  38176  dihord2pre  38421  dihord6apre  38452  dihord5b  38455  dihord5apre  38458  dihord  38460  dihmeetlem1N  38486  dihmeetlem2N  38495  dihglbcpreN  38496  dihmeetbN  38499  dihmeetlem4preN  38502  dihmeetlem5  38504  dihmeetlem6  38505  dihmeetlem7N  38506  dihmeetlem10N  38512  dihmeetlem11N  38513  dihmeetlem12N  38514  dihmeetlem13N  38515  dihmeetlem15N  38517  dihmeetlem17N  38519  dihmeetlem18N  38520  dihmeetlem19N  38521  dihmeetALTN  38523  dih1dimatlem0  38524  dihlspsnssN  38528  dvh3dim2  38644  resubcan2  39377  mzpsubst  39521  diophrw  39532  eldioph2lem1  39533  rencldnfi  39594  pellexlem2  39603  pellqrexplicit  39650  infmrgelbi  39651  rmxycomplete  39690  congadd  39739  acongeq  39756  jm2.19  39766  jm2.22  39768  jm2.20nn  39770  jm2.25lem1  39771  jm2.27  39781  jm3.1  39793  lmhmlnmsplit  39863  pwssplit4  39865  hbtlem2  39900  dgraa0p  39925  idomrootle  39971  proot1hash  39976  iocunico  39993  relexpxpmin  40250  brtrclfv2  40260  ntrclsk3  40608  grur1cld  40776  ismnu  40805  suprnmpt  41637  wessf1ornlem  41652  choicefi  41670  supxrgere  41807  supxrgelem  41811  supxrge  41812  infleinflem2  41845  snunioo1  41991  iccintsng  42002  fmul01  42064  lptre2pt  42124  0ellimcdiv  42133  fnlimfvre  42158  limsupmnfuzlem  42210  climisp  42230  limsupgtlem  42261  ibliccsinexp  42435  iblioosinexp  42437  volioc  42456  iblspltprt  42457  stoweidlem20  42504  stoweidlem22  42506  stoweidlem34  42518  stoweidlem44  42528  stoweidlem60  42544  wallispilem3  42551  fourierdlem42  42633  fourierdlem51  42641  fourierdlem54  42644  fourierdlem87  42677  fourierdlem97  42687  ioorrnopnlem  42788  sge0seq  42927  hoicvr  43029  imasetpreimafvbijlemfv  43761  lincresunit3lem3  44724  lindssnlvec  44736  rrx2linesl  44987  line2  44996  itsclc0lem3  45002  itsclc0yqsollem1  45006  itscnhlc0xyqsol  45009  itschlc0xyqsol1  45010  itsclc0  45015  itscnhlinecirc02plem2  45027  itscnhlinecirc02plem3  45028
  Copyright terms: Public domain W3C validator