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

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

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 475 . 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:  simpl3r  1109  simpr3r  1115  simp13r  1169  simp23r  1175  simp33r  1181  f1oiso2  6475  tfisi  6922  tfrlem5  7335  omeulem1  7521  omeulem2  7522  elfiun  8191  isfin2-2  8996  addid2  10065  mulcan  10508  mulcan2  10509  divass  10547  divdir  10554  div11  10557  ltdiv1  10731  ltmuldiv  10740  lediv2  10757  xaddass2  11904  xlt2add  11914  expaddz  12716  expmulz  12718  resqrex  13780  resqrtcl  13783  o1add  14133  o1mul  14134  o1sub  14135  dvdsgcd  15040  rpexp12i  15213  pythagtriplem4  15303  pythagtriplem11  15309  pythagtriplem13  15311  pcpremul  15327  pceu  15330  pcqmul  15337  pcqdiv  15341  f1ocpbllem  15948  funcoppc  16299  funcres  16320  catcisolem  16520  1stfcl  16601  2ndfcl  16602  prfcl  16607  evlfcl  16626  curf1cl  16632  curfcl  16636  hofcl  16663  latjlej12  16831  latmlem12  16847  latj4  16865  latj4rot  16866  symgsssg  17651  symgfisg  17652  odcong  17732  cmn4  17976  ablsub4  17982  abladdsub4  17983  lsm4  18027  abvdom  18602  abvtrivd  18604  lspsolvlem  18904  lbsextlem2  18921  lidlsubcl  18978  frlmbas3  19871  matinvgcell  19997  matmulcell  20007  ma1repveval  20133  mdetunilem3  20176  mdetuni0  20183  mdetmul  20185  hausflimlem  21530  psmetlecl  21867  xmetlecl  21897  prdsxmetlem  21919  xblcntrps  21961  xblcntr  21962  bndth  22491  cph2ass  22739  iscau3  22797  dvres2  23394  coemullem  23722  vieta1  23783  aalioulem4  23806  cxpcn3lem  24200  angcan  24244  divsqrtsumlem  24418  dchrmusumlema  24894  dchrvmasumlema  24901  dchrisum0lema  24915  logdivsum  24934  padicabv  25031  ax5seglem3  25524  ax5seglem6  25527  axpasch  25534  axeuclid  25556  axcontlem4  25560  axcontlem8  25564  adjlnop  28130  xreceu  28762  orngmul  28935  rhmdvd  28953  measvunilem  29403  measvuni  29405  bnj1128  30113  cgrcomim  31067  cgrcoml  31074  cgrcomr  31075  cgrdegen  31082  segconeu  31089  btwnintr  31097  btwnexch3  31098  btwnouttr2  31100  btwnouttr  31102  btwnexch  31103  ifscgr  31122  lineext  31154  linecgr  31159  lineid  31161  idinside  31162  btwnconn1lem3  31167  btwnconn1lem4  31168  btwnconn1lem14  31178  btwnconn2  31180  btwnconn3  31181  midofsegid  31182  btwnoutside  31203  outsideoftr  31207  lineunray  31225  lineelsb2  31226  itg2addnclem  32429  cnres2  32530  heibor  32588  lsmcv2  33132  lcvat  33133  lcvexchlem4  33140  lcvexchlem5  33141  lfladd  33169  lflsub  33170  lflmul  33171  lshpkrlem4  33216  latm4  33336  omlmod1i2N  33363  cvlsupr7  33451  cvlsupr8  33452  hlatj4  33476  hlrelat3  33514  cvrval3  33515  atcvrj1  33533  atlelt  33540  2atlt  33541  2atjm  33547  3noncolr2  33551  athgt  33558  3dimlem2  33561  3dimlem4OLDN  33567  1cvratex  33575  ps-1  33579  ps-2  33580  hlatexch3N  33582  llnle  33620  atcvrlln2  33621  atcvrlln  33622  lplni2  33639  lplnle  33642  lplnnle2at  33643  lplnnlelln  33645  llncvrlpln2  33659  2llnmeqat  33673  lvolnle3at  33684  lvolnlelln  33686  4atlem0ae  33696  lneq2at  33880  lnjatN  33882  lncvrat  33884  2lnat  33886  elpaddri  33904  paddasslem2  33923  padd4N  33942  hlmod1i  33958  llnexchb2  33971  dalawlem2  33974  pclfinN  34002  pexmidlem4N  34075  pl42lem1N  34081  lhp2lt  34103  lhpexle1  34110  lhpexle2lem  34111  lhpj1  34124  lhpmcvr5N  34129  lhp2at0  34134  lhp2at0nle  34137  lhple  34144  lhpat  34145  lhpat4N  34146  4atexlemnslpq  34158  4atexlem7  34177  ltrn11  34228  ltrnle  34231  ltrnm  34233  ltrnj  34234  ltrncvr  34235  ltrnel  34241  ltrncnvel  34244  ltrncnv  34248  ltrnmwOLD  34254  trlat  34272  trl0  34273  trlnidat  34276  trlnid  34282  ltrnatlw  34286  trlne  34288  trlval4  34291  cdlemc5  34298  cdlemd2  34302  cdlemd7  34307  cdlemd8  34308  cdlemd9  34309  cdleme0c  34316  cdleme0e  34320  cdleme0fN  34321  cdleme3g  34337  cdleme3h  34338  cdleme5  34343  cdleme11c  34364  cdleme11h  34369  cdleme11j  34370  cdleme11k  34371  cdleme0nex  34393  cdleme18a  34394  cdleme22gb  34397  cdleme20zN  34404  cdleme20yOLD  34406  cdleme20c  34415  cdleme20k  34423  cdleme21a  34429  cdleme21b  34430  cdleme21c  34431  cdleme21ct  34433  cdleme21h  34438  cdleme22d  34447  cdleme22f  34450  cdleme26ee  34464  cdleme30a  34482  cdlemefs45eN  34535  cdleme36a  34564  cdleme36m  34565  cdleme39a  34569  cdleme42b  34582  cdleme43dN  34596  cdlemeg47rv2  34614  cdlemeg46sfg  34624  cdlemeg46rjgN  34626  cdlemeg46rgv  34632  cdlemeg46req  34633  cdlemeg46gfv  34634  cdleme48d  34639  cdleme50ltrn  34661  cdlemf1  34665  cdlemf  34667  cdlemg2dN  34694  cdlemg2fvlem  34698  cdlemg2l  34707  cdlemg7fvbwN  34711  cdlemg7aN  34729  cdlemg10c  34743  cdlemg17a  34765  cdlemg17dALTN  34768  cdlemg18a  34782  cdlemg18b  34783  cdlemg31b0a  34799  cdlemg31a  34801  cdlemg31b  34802  ltrnco  34823  cdlemg48  34841  tgrpov  34852  tendoco2  34872  tendoplco2  34883  cdlemh1  34919  cdlemk1  34935  cdlemk26b-3  35009  cdlemk27-3  35011  cdlemk28-3  35012  cdlemk34  35014  cdlemkfid1N  35025  cdlemkid3N  35037  cdlemkid4  35038  cdlemk35s-id  35042  cdlemk39s-id  35044  cdlemk51  35057  tendospcanN  35128  cdlemm10N  35223  dicvaddcl  35295  dicvscacl  35296  cdlemn6  35307  dihvalcq2  35352  dihord6b  35365  dihord5apre  35367  dihglbcpreN  35405  dihjatc1  35416  dihmeetlem20N  35431  dih1dimatlem0  35433  dihglblem6  35445  dochexmidlem4  35568  mapdpglem32  35810  mapdh8ad  35884  mapdh9aOLDN  35896  hdmap11lem2  35950  hdmap14lem6  35981  mzpmfp  36126  mzpsubst  36127  pellex  36215  pellfundex  36266  pellfund14gap  36267  qirropth  36289  rmxypos  36330  congmul  36350  congsub  36353  mzpcong  36355  coprmdvdsb  36368  jm2.15nn0  36386  jm2.16nn0  36387  rpnnen3lem  36414  idomsubgmo  36593  relexp01min  36822  mullimc  38482  islptre  38485  mullimcf  38489  addlimc  38514  0ellimcdiv  38515  fourierdlem48  38846  fourierdlem80  38878  opnvonmbllem2  39322  ovolval5lem3  39343  ovnovollem3  39347  trlsonistrl  40913  pthonispth-av  40949  spthonisspth-av  40953  wspthneq1eq2  41053  lincfsuppcl  41993  lindslinindimp2lem3  42040
  Copyright terms: Public domain W3C validator