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

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

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 485 . 2 ((𝜒𝜃) → 𝜃)
213ad2ant3 1129 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 1083
This theorem is referenced by:  simp13r  1283  simp23r  1289  simp33r  1295  f1oiso2  7100  tfisi  7564  tfrlem5  8010  omeulem1  8201  omeulem2  8202  elfiun  8886  isfin2-2  9733  addid2  10815  mulcan  11269  mulcan2  11270  divass  11308  divdir  11315  div11  11318  ltdiv1  11496  ltmuldiv  11505  lediv2  11522  xaddass2  12636  xlt2add  12646  expaddz  13466  expmulz  13468  resqrex  14603  resqrtcl  14606  o1add  14963  o1mul  14964  o1sub  14965  dvdsgcd  15884  rpexp12i  16058  pythagtriplem4  16148  pythagtriplem11  16154  pythagtriplem13  16156  pcpremul  16172  pceu  16175  pcqmul  16182  pcqdiv  16186  f1ocpbllem  16789  funcoppc  17137  funcres  17158  catcisolem  17358  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  latjlej12  17669  latmlem12  17685  latj4  17703  latj4rot  17704  symgsssg  18517  symgfisg  18518  odcong  18599  cmn4  18848  ablsub4  18855  abladdsub4  18856  lsm4  18902  abvdom  19531  abvtrivd  19533  lspsolvlem  19836  lbsextlem2  19853  lidlsubcl  19910  frlmbas3  20836  matinvgcell  20960  matmulcell  20970  ma1repveval  21096  mdetunilem3  21139  mdetuni0  21146  mdetmul  21148  hausflimlem  22503  psmetlecl  22840  xmetlecl  22871  prdsxmetlem  22893  xblcntrps  22935  xblcntr  22936  bndth  23477  cph2ass  23732  iscau3  23796  dvres2  24425  coemullem  24755  vieta1  24816  aalioulem4  24839  cxpcn3lem  25241  angcan  25293  divsqrtsumlem  25471  dchrmusumlema  25983  dchrvmasumlema  25990  dchrisum0lema  26004  logdivsum  26023  padicabv  26120  ax5seglem3  26631  ax5seglem6  26634  axpasch  26641  axeuclid  26663  axcontlem4  26667  axcontlem8  26671  trlsonistrl  27404  pthonispth  27441  spthonisspth  27445  wspthneq1eq2  27552  frgr2wwlkeqm  28024  adjlnop  29777  xreceu  30512  orngmul  30790  rhmdvd  30808  measvunilem  31357  measvuni  31359  bnj1128  32146  umgr2cycl  32272  satfv1fvfmla1  32554  cgrcomim  33334  cgrcoml  33341  cgrcomr  33342  cgrdegen  33349  segconeu  33356  btwnintr  33364  btwnexch3  33365  btwnouttr2  33367  btwnouttr  33369  btwnexch  33370  ifscgr  33389  lineext  33421  linecgr  33426  lineid  33428  idinside  33429  btwnconn1lem3  33434  btwnconn1lem4  33435  btwnconn1lem14  33445  btwnconn2  33447  btwnconn3  33448  midofsegid  33449  btwnoutside  33470  outsideoftr  33474  lineunray  33492  lineelsb2  33493  itg2addnclem  34810  cnres2  34909  heibor  34967  lsmcv2  36032  lcvat  36033  lcvexchlem4  36040  lcvexchlem5  36041  lfladd  36069  lflsub  36070  lflmul  36071  lshpkrlem4  36116  latm4  36236  omlmod1i2N  36263  cvlsupr7  36351  cvlsupr8  36352  hlatj4  36377  hlrelat3  36415  cvrval3  36416  atcvrj1  36434  atlelt  36441  2atlt  36442  2atjm  36448  3noncolr2  36452  athgt  36459  3dimlem2  36462  3dimlem4OLDN  36468  1cvratex  36476  ps-1  36480  ps-2  36481  hlatexch3N  36483  llnle  36521  atcvrlln2  36522  atcvrlln  36523  lplni2  36540  lplnle  36543  lplnnle2at  36544  lplnnlelln  36546  llncvrlpln2  36560  2llnmeqat  36574  lvolnle3at  36585  lvolnlelln  36587  4atlem0ae  36597  lneq2at  36781  lnjatN  36783  lncvrat  36785  2lnat  36787  elpaddri  36805  paddasslem2  36824  padd4N  36843  hlmod1i  36859  llnexchb2  36872  dalawlem2  36875  pclfinN  36903  pexmidlem4N  36976  pl42lem1N  36982  lhp2lt  37004  lhpexle1  37011  lhpexle2lem  37012  lhpj1  37025  lhpmcvr5N  37030  lhp2at0  37035  lhp2at0nle  37038  lhple  37045  lhpat  37046  lhpat4N  37047  4atexlemnslpq  37059  4atexlem7  37078  ltrn11  37129  ltrnle  37132  ltrnm  37134  ltrnj  37135  ltrncvr  37136  ltrnel  37142  ltrncnvel  37145  ltrncnv  37149  trlat  37172  trl0  37173  trlnidat  37176  trlnid  37182  ltrnatlw  37186  trlne  37188  trlval4  37191  cdlemc5  37198  cdlemd2  37202  cdlemd7  37207  cdlemd8  37208  cdlemd9  37209  cdleme0c  37216  cdleme0e  37220  cdleme0fN  37221  cdleme3g  37237  cdleme3h  37238  cdleme5  37243  cdleme11c  37264  cdleme11h  37269  cdleme11j  37270  cdleme11k  37271  cdleme0nex  37293  cdleme18a  37294  cdleme22gb  37297  cdleme20zN  37304  cdleme20c  37314  cdleme20k  37322  cdleme21a  37328  cdleme21b  37329  cdleme21c  37330  cdleme21ct  37332  cdleme21h  37337  cdleme22d  37346  cdleme22f  37349  cdleme26ee  37363  cdleme30a  37381  cdlemefs45eN  37434  cdleme36a  37463  cdleme36m  37464  cdleme39a  37468  cdleme42b  37481  cdleme43dN  37495  cdlemeg47rv2  37513  cdlemeg46sfg  37523  cdlemeg46rjgN  37525  cdlemeg46rgv  37531  cdlemeg46req  37532  cdlemeg46gfv  37533  cdleme48d  37538  cdleme50ltrn  37560  cdlemf1  37564  cdlemf  37566  cdlemg2dN  37593  cdlemg2fvlem  37597  cdlemg2l  37606  cdlemg7fvbwN  37610  cdlemg7aN  37628  cdlemg10c  37642  cdlemg17a  37664  cdlemg17dALTN  37667  cdlemg18a  37681  cdlemg18b  37682  cdlemg31b0a  37698  cdlemg31a  37700  cdlemg31b  37701  ltrnco  37722  cdlemg48  37740  tgrpov  37751  tendoco2  37771  tendoplco2  37782  cdlemh1  37818  cdlemk1  37834  cdlemk26b-3  37908  cdlemk27-3  37910  cdlemk28-3  37911  cdlemk34  37913  cdlemkfid1N  37924  cdlemkid3N  37936  cdlemkid4  37937  cdlemk35s-id  37941  cdlemk39s-id  37943  cdlemk51  37956  tendospcanN  38026  cdlemm10N  38121  dicvaddcl  38193  dicvscacl  38194  cdlemn6  38205  dihvalcq2  38250  dihord6b  38263  dihord5apre  38265  dihglbcpreN  38303  dihjatc1  38314  dihmeetlem20N  38329  dih1dimatlem0  38331  dihglblem6  38343  dochexmidlem4  38466  mapdpglem32  38708  mapdh8ad  38782  mapdh9aOLDN  38793  hdmap11lem2  38845  hdmap14lem6  38876  frlmfzowrdb  39006  mzpmfp  39205  mzpsubst  39206  pellex  39293  pellfundex  39344  pellfund14gap  39345  qirropth  39366  rmxypos  39405  congmul  39425  congsub  39428  mzpcong  39430  coprmdvdsb  39443  jm2.15nn0  39461  jm2.16nn0  39462  rpnnen3lem  39489  idomsubgmo  39659  relexp01min  39919  mullimc  41758  islptre  41761  mullimcf  41765  addlimc  41790  0ellimcdiv  41791  limsupre3lem  41874  limsupre3uzlem  41877  fourierdlem48  42301  fourierdlem80  42333  opnvonmbllem2  42777  ovolval5lem3  42798  ovnovollem3  42802  lincfsuppcl  44296  lindslinindimp2lem3  44343  itsclc0lem1  44571  itsclc0lem2  44572  itschlc0yqe  44575  itsclc0xyqsolr  44584
  Copyright terms: Public domain W3C validator